1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl
  5  
  6  Some big operators for lists and finite sets.
  7  -/
  8  import tactic.tauto data.list.basic data.finset data.nat.enat
src         └──────────┘ └─────────────┘ └─────────┘ └───────────┘
  9  import algebra.group algebra.ordered_group algebra.group_power
src         └───────────┘ └───────────────────┘ └─────────────────┘
 10  
 11  universes u v w
 12  variables {α : Type u} {β : Type v} {γ : Type w}
 13  
 14  theorem directed.finset_le {r : α → α → Prop} [is_trans α r]
id                                                └──────┘  
src                                                 └──────┘
typ                                               └──────┘  
 15    {ι} (hι : nonempty ι) {f : ι → α} (D : directed r f) (s : finset ι) :
id               └──────┘                  └──────┘         └────┘ 
src              └──────┘                     └──────┘           └────┘
typ              └──────┘                  └──────┘         └────┘ 
doc                                           └──────┘           └────┘
 16    ∃ z, ∀ i ∈ s, r (f i) (f z) :=
id                     
src         
typ                    
 17  show ∃ z, ∀ i ∈ s.1, r (f i) (f z), from
id                         
src                 
typ                        
 18  multiset.induction_on s.1 (let ⟨z⟩ := hι in ⟨z, λ _, false.elim⟩) $
id   └───────────────────┘    └─┘       └┘            └────────┘
src  └───────────────────┘                               └────────┘
typ  └───────────────────┘    └─┘       └┘            └────────┘
 19  λ i s ⟨j, H⟩, let ⟨k, h₁, h₂⟩ := D i j in
id            └─┘    └┘  └┘      
typ           └─┘    └┘  └┘      
 20  ⟨k, λ a h, or.cases_on (multiset.mem_cons.1 h)
id            └─────────┘  └───────────────┘  
src             └─────────┘  └───────────────┘
typ           └─────────┘  └───────────────┘  
 21    (λ h, h.symm ▸ h₁)
id          └───┘ 
src           └───┘ 
typ         └───┘ 
 22    (λ h, trans (H _ h) h₂)⟩
id          └───┘      
src          └───┘
typ         └───┘      
 23  
 24  theorem finset.exists_le {α : Type u} [nonempty α] [directed_order α] (s : finset α) :
id                                          └──────┘    └────────────┘        └────┘ 
src                                         └──────┘     └────────────┘         └────┘
typ                                         └──────┘    └────────────┘        └────┘ 
doc                                                                             └────┘
 25    ∃ M, ∀ i ∈ s, i ≤ M :=
id                
src                  
typ               
 26  directed.finset_le (by apply_instance) directed_order.directed s
id   └────────────────┘                     └─────────────────────┘ 
src  └────────────────┘     └────────────┘  └─────────────────────┘
typ  └────────────────┘     └────────────┘  └─────────────────────┘ 
doc                         └────────────┘
txt                         └────────────┘
par                         └────────────┘
st                         └─────────────┘
 27  
 28  namespace finset
 29  variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
id                        └────┘
src                       └────┘
typ                       └────┘
doc                       └────┘
 30  
 31  /-- `prod s f` is the product of `f x` as `x` ranges over the elements of the finite set `s`. -/
 32  @[to_additive]
doc    └─────────┘
 33  protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1.map f).prod
id                       └─────────┘        └────┘                     └─┘   └──┘
src                      └─────────┘         └────┘                          └─┘    └──┘
typ                      └─────────┘        └────┘                     └─┘   └──┘
doc                                          └────┘                           └─┘    └──┘
 34  
 35  @[to_additive] lemma prod_eq_multiset_prod [comm_monoid β] (s : finset α) (f : α → β) :
id                                               └─────────┘        └────┘           
src                                              └─────────┘         └────┘
typ                                              └─────────┘        └────┘           
doc    └─────────┘                                                   └────┘
 36    s.prod f = (s.1.map f).prod := rfl
id     └───┘     └─┘   └──┘     └─┘
src     └───┘       └─┘    └──┘     └─┘
typ    └───┘     └─┘   └──┘     └─┘
doc     └───┘         └─┘    └──┘
 37  
 38  @[to_additive]
doc    └─────────┘
 39  theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) : s.prod f = s.fold (*) 1 f := rfl
id                         └─────────┘        └────┘               └───┘   └───┘          └─┘
src                        └─────────┘         └────┘                   └───┘     └───┘           └─┘
typ                        └─────────┘        └────┘               └───┘   └───┘          └─┘
doc                                            └────┘                   └───┘      └───┘
 40  
 41  section comm_monoid
 42  variables [comm_monoid β]
id              └─────────┘
src             └─────────┘
typ             └─────────┘
 43  
 44  @[simp, to_additive]
doc    └──┘  └─────────┘
 45  lemma prod_empty {α : Type u} {f : α → β} : (∅:finset α).prod f = 1 := rfl
id                                               └────┘  └──┘         └─┘
src                                                └────┘   └──┘          └─┘
typ                                              └────┘  └──┘         └─┘
doc                                                 └────┘   └──┘
 46  
 47  @[simp, to_additive]
doc    └──┘  └─────────┘
 48  lemma prod_insert [decidable_eq α] : a ∉ s → (insert a s).prod f = f a * s.prod f := fold_insert
id                      └──────────┘           └────┘   └──┘       └───┘     └─────────┘
src                     └──────────┘              └────┘     └──┘           └───┘      └─────────┘
typ                     └──────────┘           └────┘   └──┘       └───┘     └─────────┘
doc                                                           └──┘             └───┘
 49  
 50  @[simp, to_additive]
doc    └──┘  └─────────┘
 51  lemma prod_singleton : (singleton a).prod f = f a :=
id                           └───────┘  └──┘     
src                          └───────┘   └──┘    
typ                          └───────┘  └──┘     
doc                          └───────┘   └──┘
 52  eq.trans fold_singleton $ mul_one _
id   └──────┘ └────────────┘   └─────┘
src  └──────┘ └────────────┘   └─────┘
typ  └──────┘ └────────────┘   └─────┘
 53  
 54  @[to_additive]
doc    └─────────┘
 55  lemma prod_pair [decidable_eq α] {a b : α} (h : a ≠ b) :
 56    ({a, b} : finset α).prod f = f a * f b :=
 57  by simp [prod_insert (not_mem_singleton.2 h.symm), mul_comm]
id            └─────────┘  └───────────────┘   └────┘   └──────┘
src     └────┘└─────────┘ └───────────────┘└─┘└────┘└─┘└──────┘└─
typ     └────┘└─────────┘ └───────────────┘└─┘└────┘└─┘└──────┘└─
doc     └────┘                             └─┘      └─┘        └─
txt     └────┘                             └─┘      └─┘        └─
par     └────┘                             └─┘      └─┘        └─
pid                                      └─┘      └─┘        
st          └─────────────────────────────────────────────────────
 58  
src  
typ  
doc  
txt  
par  
pid  
st   
 59  @[simp] lemma prod_const_one : s.prod (λx, (1 : β)) = 1 :=
id                                  └───┘             
src                                  └───┘               
typ                                 └───┘             
doc    └──┘                          └───┘
 60  by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow]
id                 └─────────┘  └────────────────┘  └──────────────────┘  └─────┘
src     └─────────┘└─────────┘└┘└────────────────┘└┘└──────────────────┘└┘└─────┘└┘
typ     └─────────┘└─────────┘└┘└────────────────┘└┘└──────────────────┘└┘└─────┘└┘
doc     └─────────┘└─────────┘└┘                  └┘                    └┘       └┘
txt     └─────────┘           └┘                  └┘                    └┘       └┘
par     └─────────┘           └┘                  └┘                    └┘       └┘
pid         └──┘└┘           └┘                  └┘                    └┘       
st     └──────────────────────────────────────────────────────────────────────────┘
 61  @[simp] lemma sum_const_zero {β} {s : finset α} [add_comm_monoid β] : s.sum (λx, (0 : β)) = 0 :=
id                                         └────┘    └─────────────┘     └──┘             
src                                        └────┘     └─────────────┘       └──┘               
typ                                        └────┘    └─────────────┘     └──┘             
doc    └──┘                                └────┘
 62  @prod_const_one _ (multiplicative β) _ _
id    └────────────┘    └────────────┘ 
src   └────────────┘    └────────────┘
typ   └────────────┘    └────────────┘ 
 63  attribute [to_additive] prod_const_one
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
doc             └─────────┘
 64  
 65  @[simp, to_additive]
doc    └──┘  └─────────┘
 66  lemma prod_image [decidable_eq α] {s : finset γ} {g : γ → α} :
id                     └──────────┘        └────┘           
src                    └──────────┘         └────┘
typ                    └──────────┘        └────┘           
doc                                         └────┘
 67    (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).prod f = s.prod (λx, f (g x)) :=
id                            └────┘  └──┘    └───┘        
src                                      └────┘   └──┘      └───┘
typ                           └────┘  └──┘    └───┘        
doc                                        └────┘   └──┘       └───┘
 68  fold_image
id   └────────┘
src  └────────┘
typ  └────────┘
 69  
 70  @[simp, to_additive]
doc    └──┘  └─────────┘
 71  lemma prod_map (s : finset α) (e : α ↪ γ) (f : γ → β) :
id                       └────┘                    
src                      └────┘           
typ                      └────┘                    
doc                      └────┘
 72    (s.map e).prod f = s.prod (λa, f (e a)) :=
id      └──┘  └──┘    └───┘        
src      └──┘   └──┘      └───┘
typ     └──┘  └──┘    └───┘        
doc             └──┘       └───┘
 73  by rw [finset.prod, finset.map_val, multiset.map_map]; refl
id          └─────────┘  └────────────┘  └──────────────┘
src     └──┘└─────────┘└┘└────────────┘└┘└──────────────┘  └────
typ     └──┘└─────────┘└┘└────────────┘└┘└──────────────┘  └────
doc     └──┘└─────────┘└┘              └┘                  └────
txt     └──┘           └┘              └┘                  └────
par     └──┘           └┘              └┘                  └────
pid       └┘           └┘              └┘                      
st     └──────────────┘└──────────────┘└────────────────┘└──────
 74  
src  
typ  
doc  
txt  
par  
pid  
st   
 75  @[congr, to_additive]
src    └───┘
doc    └───┘  └─────────┘
 76  lemma prod_congr (h : s₁ = s₂) : (∀x∈s₂, f x = g x) → s₁.prod f = s₂.prod g :=
id                         └┘  └┘       └┘          └┘└───┘   └┘└───┘ 
src                                                        └───┘      └───┘
typ                        └┘  └┘       └┘          └┘└───┘   └┘└───┘ 
doc                                                          └───┘       └───┘
 77  by rw [h]; exact fold_congr
id                   └────────┘
src     └──┘   └────┘└────────┘
typ     └──┘  └────┘└────────┘
doc     └──┘   └────┘          
txt     └──┘   └────┘          
par     └──┘   └────┘          
pid       └┘                  
st     └────┘└─────────────────┘
 78  attribute [congr] finset.sum_congr
id                     └──────────────┘
src             └───┘  └──────────────┘
typ                    └──────────────┘
doc             └───┘
 79  
 80  @[to_additive]
doc    └─────────┘
 81  lemma prod_union_inter [decidable_eq α] : (s₁ ∪ s₂).prod f * (s₁ ∩ s₂).prod f = s₁.prod f * s₂.prod f :=
id                           └──────────┘      └┘  └┘ └──┘     └┘  └┘ └──┘    └┘└───┘   └┘└───┘ 
src                          └──────────┘              └──┘             └──┘       └───┘      └───┘
typ                          └──────────┘      └┘  └┘ └──┘     └┘  └┘ └──┘    └┘└───┘   └┘└───┘ 
doc                                                     └──┘               └──┘        └───┘       └───┘
 82  fold_union_inter
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
 83  
 84  @[to_additive]
doc    └─────────┘
 85  lemma prod_union [decidable_eq α] (h : disjoint s₁ s₂) : (s₁ ∪ s₂).prod f = s₁.prod f * s₂.prod f :=
id                     └──────────┘        └──────┘ └┘ └┘     └┘  └┘ └──┘    └┘└───┘   └┘└───┘ 
src                    └──────────┘         └──────┘                  └──┘       └───┘      └───┘
typ                    └──────────┘        └──────┘ └┘ └┘     └┘  └┘ └──┘    └┘└───┘   └┘└───┘ 
doc                                         └──────┘                   └──┘        └───┘       └───┘
 86  by rw [←prod_union_inter, (disjoint_iff_inter_eq_empty.mp h)]; exact (mul_one _).symm
id           └──────────────┘   └────────────────────────────┘            └─────┘
src     └───┘└──────────────┘└┘ └────────────────────────────┘ └┘  └────┘ └─────┘└────────
typ     └───┘└──────────────┘└┘ └────────────────────────────┘└┘  └────┘ └─────┘└────────
doc     └───┘                └┘                                └┘  └────┘        └────────
txt     └───┘                └┘                                └┘  └────┘        └────────
par     └───┘                └┘                                └┘  └────┘        └────────
pid       └─┘                └┘                                └┘               └─────┘└─
st     └────────────────────┘└──────────────────────────────────┘└────────────────────────
 87  
src  
typ  
doc  
txt  
par  
pid  
st   
 88  @[to_additive]
doc    └─────────┘
 89  lemma prod_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) : (s₂ \ s₁).prod f * s₁.prod f = s₂.prod f :=
id                     └──────────┘        └┘  └┘     └┘  └┘ └──┘    └┘└───┘   └┘└───┘ 
src                    └──────────┘                           └──┘       └───┘      └───┘
typ                    └──────────┘        └┘  └┘     └┘  └┘ └──┘    └┘└───┘   └┘└───┘ 
doc                                                             └──┘        └───┘       └───┘
 90  by rw [←prod_union sdiff_disjoint, sdiff_union_of_subset h]
id           └────────┘ └────────────┘  └───────────────────┘ 
src     └───┘└────────┘└────────────┘└┘└───────────────────┘ └─
typ     └───┘└────────┘└────────────┘└┘└───────────────────┘└─
doc     └───┘                        └┘                      └─
txt     └───┘                        └┘                      └─
par     └───┘                        └┘                      └─
pid       └─┘                        └┘                      
st     └─────────────────────────────┘└───────────────────────┘
 91  
src  
typ  
doc  
txt  
par  
pid  
st   
 92  @[simp, to_additive]
doc    └──┘  └─────────┘
 93  lemma prod_sum_elim [decidable_eq (α ⊕ γ)]
id                        └──────────┘    
src                       └──────────┘    
typ                       └──────────┘    
 94    (s : finset α) (t : finset γ) (f : α → β) (g : γ → β) :
id          └────┘        └────┘                     
src         └────┘         └────┘
typ         └────┘        └────┘                     
doc         └────┘         └────┘
 95    (s.image sum.inl ∪ t.image sum.inr).prod (sum.elim f g) = s.prod f * t.prod g :=
id      └────┘ └─────┘  └────┘ └─────┘ └──┘   └──────┘     └───┘   └───┘ 
src      └────┘ └─────┘   └────┘ └─────┘ └──┘   └──────┘        └───┘     └───┘
typ     └────┘ └─────┘  └────┘ └─────┘ └──┘   └──────┘     └───┘   └───┘ 
doc      └────┘            └────┘         └──┘                    └───┘      └───┘
 96  begin
st   └─────
 97    rw [prod_union, prod_image, prod_image],
id         └────────┘  └────────┘  └────────┘
src    └──┘└────────┘└┘└────────┘└┘└────────┘
typ    └──┘└────────┘└┘└────────┘└┘└────────┘
doc    └──┘          └┘          └┘          
txt    └──┘          └┘          └┘          
par    └──┘          └┘          └┘          
pid      └┘          └┘          └┘          
st   ───────────────┘└──────────┘└──────────┘└──
 98    { simp only [sum.elim_inl, sum.elim_inr] },
id                  └──────────┘  └──────────┘
src      └─────────┘└──────────┘└┘└──────────┘└┘
typ      └─────────┘└──────────┘└┘└──────────┘└┘
doc      └─────────┘            └┘            └┘
txt      └─────────┘            └┘            └┘
par      └─────────┘            └┘            └┘
pid          └──┘└┘            └┘            
st   ───┘└─────────────────────────────────────┘└┘
 99    { exact λ _ _ _ _, sum.inr.inj },
id                        └─────────┘
src      └────┘ └────────┘└─────────┘
typ      └────┘ └────────┘└─────────┘
doc      └────┘ └────────┘           
txt      └────┘ └────────┘           
par      └────┘ └────────┘           
pid            └────────┘           
st   ───┘└───────────────────────────┘└┘
100    { exact λ _ _ _ _, sum.inl.inj },
id                        └─────────┘
src      └────┘ └────────┘└─────────┘
typ      └────┘ └────────┘└─────────┘
doc      └────┘ └────────┘           
txt      └────┘ └────────┘           
par      └────┘ └────────┘           
pid            └────────┘           
st   ───┘└───────────────────────────┘└┘
101    { rintros i hi,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid             └───┘
st   ───────────────┘└─
102      erw [finset.mem_inter, finset.mem_image, finset.mem_image] at hi,
id            └──────────────┘  └──────────────┘  └──────────────┘
src      └───┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└─────┘
typ      └───┘└──────────────┘└┘└──────────────┘└┘└──────────────┘└─────┘
doc      └───┘                └┘                └┘                └─────┘
txt      └───┘                └┘                └┘                └─────┘
par      └───┘                └┘                └┘                └─────┘
pid         └┘                └┘                └┘                └────┘
st   ────────────────────────┘└────────────────┘└────────────────┘└────┘└─
103      rcases hi with ⟨⟨i, hi, rfl⟩, ⟨j, hj, H⟩⟩,
id              └┘
src      └─────┘  └──────────────────────────────┘
typ      └─────┘└┘└──────────────────────────────┘
doc      └─────┘  └──────────────────────────────┘
txt      └─────┘  └──────────────────────────────┘
par      └─────┘  └──────────────────────────────┘
pid              └──────────────────────────────┘
st   ────────────────────────────────────────────┘└─
104      cases H }
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───────────┘└─
105  end
st   ──┘
106  
107  @[to_additive]
doc    └─────────┘
108  lemma prod_bind [decidable_eq α] {s : finset γ} {t : γ → finset α} :
id                    └──────────┘        └────┘           └────┘ 
src                   └──────────┘         └────┘             └────┘
typ                   └──────────┘        └────┘           └────┘ 
doc                                        └────┘             └────┘
109    (∀x∈s, ∀y∈s, x ≠ y → disjoint (t x) (t y)) → (s.bind t).prod f = s.prod (λx, (t x).prod f) :=
id                   └──────┘             └───┘  └──┘    └───┘        └──┘  
src                        └──────┘                  └───┘   └──┘      └───┘           └──┘
typ                  └──────┘             └───┘  └──┘    └───┘        └──┘  
doc                         └──────┘                  └───┘   └──┘       └───┘           └──┘
110  by haveI := classical.dec_eq γ; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
111  finset.induction_on s (λ _, by simp only [bind_empty, prod_empty])
id   └─────────────────┘                      └────────┘  └────────┘
src  └─────────────────┘   └──┘  └─────────┘└────────┘└┘└────────┘└─
typ  └─────────────────┘  └──┘  └─────────┘└────────┘└┘└────────┘└─
doc  └─────────────────┘   └──┘  └─────────┘          └┘          └─
txt                        └──┘  └─────────┘          └┘          └─
par                        └──┘  └─────────┘          └┘          └─
pid                        └──┘  └──────────┘          └┘          └──
st   ─────────────────────────────┘└─────────────────────────────────┘└─
112    (assume x s hxs ih hd,
src  ─┘       └───────────────
typ  ─┘       └───────────────
doc  ─┘       └───────────────
txt  ─┘       └───────────────
par  ─┘       └───────────────
pid  ─┘       └───────────────
st   ─────────────────────────
113    have hd' : ∀x∈s, ∀y∈s, x ≠ y → disjoint (t x) (t y),
id                              
src  ─┘    └─────┘ └┘   └┘                └┘   └──
typ  ─┘    └─────┘ └┘   └┘                └┘   └──
doc  ─┘    └─────┘ └┘   └┘                 └┘   └──
txt  ─┘    └─────┘ └┘   └┘                 └┘   └──
par  ─┘    └─────┘ └┘   └┘                 └┘   └──
pid  ─┘    └─────┘ └┘   └┘                 └┘   └──
st   ───────────────────────────────────────────────────────
114      from assume _ hx _ hy, hd _ (mem_insert_of_mem hx) _ (mem_insert_of_mem hy),
id                                                             └───────────────┘
src  ────────┘      └──────────┘  └─┘                    └──┘ └───────────────┘  └──
typ  ────────┘      └──────────┘  └─┘                    └──┘ └───────────────┘  └──
doc  ────────┘      └──────────┘  └─┘                    └──┘                    └──
txt  ────────┘      └──────────┘  └─┘                    └──┘                    └──
par  ────────┘      └──────────┘  └─┘                    └──┘                    └──
pid  ────────┘      └──────────┘  └─┘                    └──┘                    └──
st   ─────────────────────────────────────────────────────────────────────────────────
115    have ∀y∈s, x ≠ y,
src  ─┘     └┘     └─
typ  ─┘     └┘     └─
doc  ─┘     └┘     └─
txt  ─┘     └┘     └─
par  ─┘     └┘     └─
pid  ─┘     └┘     └─
st   ────────────────────
116      from assume _ hy h, by rw [←h] at hy; contradiction,
id                                   
src  ────────┘      └───────┘  └───┘ └─────┘└┘└───────────┘└─
typ  ────────┘      └───────┘  └───┘└─────┘└┘└───────────┘└─
doc  ────────┘      └───────┘  └───┘ └─────┘└┘└───────────┘└─
txt  ────────┘      └───────┘  └───┘ └─────┘└┘└───────────┘└─
par  ────────┘      └───────┘  └───┘ └─────┘└┘└───────────┘└─
pid  ────────┘      └───────┘  └────┘ └───────────────────────
st   ─────────────────────────┘└─────┘└───────────────────┘└─
117    have ∀y∈s, disjoint (t x) (t y),
src  ─┘     └┘             └┘   └──
typ  ─┘     └┘             └┘   └──
doc  ─┘     └┘             └┘   └──
txt  ─┘     └┘             └┘   └──
par  ─┘     └┘             └┘   └──
pid  ─┘     └┘             └┘   └──
st   ───────────────────────────────────
118      from assume _ hy, hd _ (mem_insert_self _ _) _ (mem_insert_of_mem hy) (this _ hy),
id                               └─────────────┘
src  ────────┘      └─────┘  └─┘ └─────────────┘└──────┘                    └┘     └─┘  └──
typ  ────────┘      └─────┘  └─┘ └─────────────┘└──────┘                    └┘     └─┘  └──
doc  ────────┘      └─────┘  └─┘                └──────┘                    └┘     └─┘  └──
txt  ────────┘      └─────┘  └─┘                └──────┘                    └┘     └─┘  └──
par  ────────┘      └─────┘  └─┘                └──────┘                    └┘     └─┘  └──
pid  ────────┘      └─────┘  └─┘                └──────┘                    └┘     └─┘  └──
st   ───────────────────────────────────────────────────────────────────────────────────────
119    have disjoint (t x) (finset.bind s t),
id                          └─────────┘   
src  ─┘    └────────┘   └┘ └─────────┘  └──
typ  ─┘    └────────┘   └┘ └─────────┘ └──
doc  ─┘    └────────┘   └┘ └─────────┘  └──
txt  ─┘    └────────┘   └┘              └──
par  ─┘    └────────┘   └┘              └──
pid  ─┘    └────────┘   └┘              └──
st   ─────────────────────────────────────────
120      from (disjoint_bind_right _ _ _).mpr this,
id             └─────────────────┘
src  ────────┘ └─────────────────┘└──────────┘    └─
typ  ────────┘ └─────────────────┘└──────────┘    └─
doc  ────────┘                    └──────────┘    └─
txt  ────────┘                    └──────────┘    └─
par  ────────┘                    └──────────┘    └─
pid  ────────┘                    └──────────┘    └─
st   ───────────────────────────────────────────────
121    by simp only [bind_insert, prod_insert hxs, prod_union this, ih hd'])
id                   └─────────┘  └─────────┘ └─┘  └────────┘ └──┘  └┘ └─┘
src  ─┘  └─────────┘└─────────┘└┘└─────────┘   └┘└────────┘    └┘     └─
typ  ─┘  └─────────┘└─────────┘└┘└─────────┘└─┘└┘└────────┘└──┘└┘└┘└─┘└─
doc  ─┘  └─────────┘           └┘              └┘              └┘     └─
txt  ─┘  └─────────┘           └┘              └┘              └┘     └─
par  ─┘  └─────────┘           └┘              └┘              └┘     └─
pid  ─┘  └──────────┘           └┘              └┘              └┘     └┘
st   ───┘└────────────────────────────────────────────────────────────────┘└─
122  
src  
typ  
doc  
txt  
par  
pid  
st   
123  @[to_additive]
doc    └─────────┘
124  lemma prod_product {s : finset γ} {t : finset α} {f : γ×α → β} :
id                           └────┘        └────┘           
src                          └────┘         └────┘          
typ                          └────┘        └────┘           
doc                          └────┘         └────┘
125    (s.product t).prod f = s.prod (λx, t.prod $ λy, f (x, y)) :=
id      └──────┘  └──┘    └───┘     └───┘         
src      └──────┘   └──┘      └───┘       └───┘         
typ     └──────┘  └──┘    └───┘     └───┘         
doc      └──────┘   └──┘       └───┘       └───┘
126  begin
st   └─────
127    haveI := classical.dec_eq α, haveI := classical.dec_eq γ,
id              └──────────────┘            └──────────────┘ 
src    └───────┘└──────────────┘   └───────┘└──────────────┘
typ    └───────┘└──────────────┘  └───────┘└──────────────┘
doc    └───────┘                   └───────┘                
txt    └───────┘                   └───────┘                
par    └───────┘                   └───────┘                
pid         └─┘                        └─┘                
st   ────────────────────────────┘└───────────────────────────┘└─
128    rw [product_eq_bind, prod_bind],
id         └─────────────┘  └───────┘
src    └──┘└─────────────┘└┘└───────┘
typ    └──┘└─────────────┘└┘└───────┘
doc    └──┘               └┘         
txt    └──┘               └┘         
par    └──┘               └┘         
pid      └┘               └┘         
st   ────────────────────┘└─────────┘└──
129    { congr, funext, exact prod_image (λ _ _ _ _ H, (prod.mk.inj H).2) },
id                            └────────┘                └─────────┘
src      └───┘  └────┘  └────┘└────────┘  └──────────┘ └─────────┘ └───┘
typ      └───┘  └────┘  └────┘└────────┘  └──────────┘ └─────────┘ └───┘
doc             └────┘  └────┘            └──────────┘             └───┘
txt      └───┘  └────┘  └────┘            └──────────┘             └───┘
par      └───┘  └────┘  └────┘            └──────────┘             └───┘
pid                                      └──────────┘             └──┘
st   ───┘└───┘└──────┘└──────────────────────────────────────────────────┘└┘
130    simp only [disjoint_iff_ne, mem_image],
id                └─────────────┘  └───────┘
src    └─────────┘└─────────────┘└┘└───────┘
typ    └─────────┘└─────────────┘└┘└───────┘
doc    └─────────┘               └┘         
txt    └─────────┘               └┘         
par    └─────────┘               └┘         
pid        └──┘└┘               └┘         
st   ───────────────────────────────────────┘└─
131    rintros _ _ _ _ h ⟨_, _⟩ ⟨_, _, ⟨_, _⟩⟩ ⟨_, _⟩ ⟨_, _, ⟨_, _⟩⟩ _,
src    └─────────────────────────────────────────────────────────────┘
typ    └─────────────────────────────────────────────────────────────┘
doc    └─────────────────────────────────────────────────────────────┘
txt    └─────────────────────────────────────────────────────────────┘
par    └─────────────────────────────────────────────────────────────┘
pid           └──────────────────────────────────────────────────────┘
st   ────────────────────────────────────────────────────────────────┘└─
132    apply h, cc
src    └────┘   └─┘
typ    └────┘   └─┘
doc    └────┘   └─┘
txt    └────┘   └─┘
par    └────┘   └─┘
pid              
st   ────────┘└───┘
133  end
st   └─┘
134  
135  @[to_additive]
doc    └─────────┘
136  lemma prod_sigma {σ : α → Type*}
id                         
typ                        
137    {s : finset α} {t : Πa, finset (σ a)} {f : sigma σ → β} :
id          └────┘           └────┘           └───┘    
src         └────┘             └────┘             └───┘
typ         └────┘           └────┘           └───┘    
doc         └────┘             └────┘
138    (s.sigma t).prod f = s.prod (λa, (t a).prod $ λs, f ⟨a, s⟩) :=
id      └────┘  └──┘    └───┘        └──┘           
src      └────┘   └──┘      └───┘           └──┘
typ     └────┘  └──┘    └───┘        └──┘           
doc      └────┘   └──┘       └───┘           └──┘
139  by haveI := classical.dec_eq α; haveI := (λ a, classical.dec_eq (σ a)); exact
id               └──────────────┘                  └──────────────┘  
src     └───────┘└──────────────┘   └───────┘  └──┘└──────────────┘   └┘  └────┘
typ     └───────┘└──────────────┘  └───────┘  └──┘└──────────────┘  └┘  └────┘
doc     └───────┘                   └───────┘  └──┘                   └┘  └────┘
txt     └───────┘                   └───────┘  └──┘                   └┘  └────┘
par     └───────┘                   └───────┘  └──┘                   └┘  └────┘
pid          └─┘                        └─┘  └──┘                   └┘       
st     └───────────────────────────────────────────────────────────────────────────
140  calc (s.sigma t).prod f =
id         └─────┘
src       └─────┘ └─────┘  
typ       └─────┘ └─────┘  
doc       └─────┘ └─────┘  
txt               └─────┘  
par               └─────┘  
pid               └─────┘  
st   ──────────────────────────
141         (s.bind (λa, (t a).image (λs, sigma.mk a s))).prod f : by rw sigma_eq_bind
id           └────┘                      └──────┘                      └───────────┘
src  ──────┘ └────┘  └─┘   └──────┘  └─┘└──────┘  └───────┘ └─┘  └─┘└───────────┘
typ  ──────┘ └────┘  └─┘  └──────┘  └─┘└──────┘  └───────┘└─┘  └─┘└───────────┘
doc  ──────┘ └────┘  └─┘   └──────┘  └─┘          └───────┘ └─┘  └─┘             
txt  ──────┘         └─┘   └──────┘  └─┘          └───────┘ └─┘  └─┘             
par  ──────┘         └─┘   └──────┘  └─┘          └───────┘ └─┘  └─┘             
pid  ──────┘         └─┘   └──────┘  └─┘          └───────┘ └─┘  └──┘             
st   ───────────────────────────────────────────────────────────────┘└─────────────────
142    ... = s.prod (λa, ((t a).image (λs, sigma.mk a s)).prod f) :
src  ─┘└──┘         └─┘    └──────┘  └─┘          └──────┘ └───
typ  ─┘└──┘         └─┘    └──────┘  └─┘          └──────┘ └───
doc  ─┘└──┘         └─┘    └──────┘  └─┘          └──────┘ └───
txt  ─┘└──┘         └─┘    └──────┘  └─┘          └──────┘ └───
par  ─┘└──┘         └─┘    └──────┘  └─┘          └──────┘ └───
pid  ─────┘         └─┘    └──────┘  └─┘          └──────┘ └───
st   ─┘└────────────────────────────────────────────────────────────
143      prod_bind $ assume a₁ ha a₂ ha₂ h,
id       └───────┘
src  ───┘└───────┘       └────────────────
typ  ───┘└───────┘       └────────────────
doc  ───┘                └────────────────
txt  ───┘                └────────────────
par  ───┘                └────────────────
pid  ───┘                └────────────────
st   ───────────────────────────────────────
144      by simp only [disjoint_iff_ne, mem_image];
id                     └─────────────┘  └───────┘
src  ───┘  └─────────┘└─────────────┘└┘└───────┘└─
typ  ───┘  └─────────┘└─────────────┘└┘└───────┘└─
doc  ───┘  └─────────┘               └┘         └─
txt  ───┘  └─────────┘               └┘         └─
par  ───┘  └─────────┘               └┘         └─
pid  ───┘  └──────────┘               └┘         └──
st   ─────┘└────────────────────────────────────────
145      rintro ⟨_, _⟩ ⟨_, _, _⟩ ⟨_, _⟩ ⟨_, _, _⟩ ⟨_, _⟩; apply h; cc
src  ───┘└─────────────────────────────────────────────┘└┘└────┘ └┘└──
typ  ───┘└─────────────────────────────────────────────┘└──────┘ └┘└──
doc  ───┘└─────────────────────────────────────────────┘└┘└────┘ └┘└──
txt  ───┘└─────────────────────────────────────────────┘└┘└────┘ └┘└──
par  ───┘└─────────────────────────────────────────────┘└──────┘ └┘└──
pid  ──────────────────────────────────────────────────────────┘ └────
st   ─────────────────────────────────────────────────────────────────
146    ... = (s.prod $ λa, (t a).prod $ λs, f ⟨a, s⟩) :
id            └────┘
src  ─┘└──┘  └────┘  └─┘   └─────┘  └─┘   └┘ └────
typ  ─┘└──┘  └────┘  └─┘   └─────┘  └─┘   └┘ └────
doc  ─┘└──┘  └────┘  └─┘   └─────┘  └─┘   └┘ └────
txt  ─┘└──┘          └─┘   └─────┘  └─┘   └┘ └────
par  ─┘└──┘          └─┘   └─────┘  └─┘   └┘ └────
pid  ─────┘          └─┘   └─────┘  └─┘   └┘ └────
st   ─┘└────────────────────────────────────────────────
147      prod_congr rfl $ λ _ _, prod_image $ λ _ _ _ _ _, by cc
id       └────────┘ └─┘          └────────┘
src  ───┘└────────┘└─┘  └────┘└────────┘  └──────────┘  └──
typ  ───┘└────────┘└─┘  └────┘└────────┘  └──────────┘  └──
doc  ───┘               └────┘            └──────────┘  └──
txt  ───┘               └────┘            └──────────┘  └──
par  ───┘               └────┘            └──────────┘  └──
pid  ───┘               └────┘            └──────────┘  └───
st   ───────────────────────────────────────────────────────┘└───
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149  @[to_additive]
doc    └─────────┘
150  lemma prod_image' [decidable_eq α] {s : finset γ} {g : γ → α} (h : γ → β)
id                      └──────────┘        └────┘                     
src                     └──────────┘         └────┘
typ                     └──────────┘        └────┘                     
doc                                          └────┘
151    (eq : ∀c∈s, f (g c) = (s.filter (λc', g c' = g c)).prod h) :
id                      └─────┘   └┘   └┘     └──┘  
src                           └─────┘                  └──┘
typ                     └─────┘   └┘   └┘     └──┘  
doc                            └─────┘                   └──┘
152    (s.image g).prod f = s.prod h :=
id      └────┘  └──┘    └───┘ 
src      └────┘   └──┘      └───┘
typ     └────┘  └──┘    └───┘ 
doc      └────┘   └──┘       └───┘
153  begin
st   └─────
154    letI := classical.dec_eq γ,
id             └──────────────┘ 
src    └──────┘└──────────────┘
typ    └──────┘└──────────────┘
doc    └──────┘                
txt    └──────┘                
par    └──────┘                
pid        └─┘                
st   ───────────────────────────┘└─
155    rw [← image_bind_filter_eq s g] {occs := occurrences.pos [2]},
id           └──────────────────┘             └─────────────┘  
src    └────┘└──────────────────┘  └┘ └──────┘└─────────────┘
typ    └────┘└──────────────────┘└┘ └──────┘└─────────────┘
doc    └────┘                      └┘ └──────┘                 
txt    └────┘                      └┘ └──────┘                 
par    └────┘                      └┘ └──────┘                 
pid      └──┘                       └──────┘                 
st   ───────────────────────────────┘└────────────────────────────┘└─
156    rw [finset.prod_bind],
id         └──────────────┘
src    └──┘└──────────────┘
typ    └──┘└──────────────┘
doc    └──┘                
txt    └──┘                
par    └──┘                
pid      └┘                
st   ─────────────────────┘└──
157    { refine finset.prod_congr rfl (assume a ha, _),
id              └───────────────┘ └─┘
src      └─────┘└───────────────┘└─┘       └───────┘
typ      └─────┘└───────────────┘└─┘       └───────┘
doc      └─────┘                           └───────┘
txt      └─────┘                           └───────┘
par      └─────┘                           └───────┘
pid                                       └───────┘
st   ───┘└───────────────────────────────────────────┘└─
158      rcases finset.mem_image.1 ha with ⟨b, hb, rfl⟩,
id              └──────────────┘   └┘
src      └─────┘└──────────────┘└─┘  └────────────────┘
typ      └─────┘└──────────────┘└─┘└┘└────────────────┘
doc      └─────┘                └─┘  └────────────────┘
txt      └─────┘                └─┘  └────────────────┘
par      └─────┘                └─┘  └────────────────┘
pid                            └─┘  └────────────────┘
st   ─────────────────────────────────────────────────┘└─
159      exact eq b hb },
id             └┘  └┘
src      └────┘└┘   
typ      └────┘└┘└┘
doc      └────┘     
txt      └────┘     
par      └────┘     
pid                
st   ─────────────────┘└┘
160    assume a₀ _ a₁ _ ne,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid    └─────────────────┘
st   ────────────────────┘└─
161    refine (disjoint_iff_ne.2 _),
id             └─────────────┘
src    └─────┘ └─────────────┘└───┘
typ    └─────┘ └─────────────┘└───┘
doc    └─────┘                └───┘
txt    └─────┘                └───┘
par    └─────┘                └───┘
pid                          └───┘
st   ─────────────────────────────┘└─
162    assume c₀ h₀ c₁ h₁,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid    └────────────────┘
st   ───────────────────┘└─
163    rcases mem_filter.1 h₀ with ⟨h₀, rfl⟩,
id            └────────┘   └┘
src    └─────┘└────────┘└─┘  └─────────────┘
typ    └─────┘└────────┘└─┘└┘└─────────────┘
doc    └─────┘          └─┘  └─────────────┘
txt    └─────┘          └─┘  └─────────────┘
par    └─────┘          └─┘  └─────────────┘
pid                    └─┘  └─────────────┘
st   ──────────────────────────────────────┘└─
164    rcases mem_filter.1 h₁ with ⟨h₁, rfl⟩,
id            └────────┘   └┘
src    └─────┘└────────┘└─┘  └─────────────┘
typ    └─────┘└────────┘└─┘└┘└─────────────┘
doc    └─────┘          └─┘  └─────────────┘
txt    └─────┘          └─┘  └─────────────┘
par    └─────┘          └─┘  └─────────────┘
pid                    └─┘  └─────────────┘
st   ──────────────────────────────────────┘└─
165    exact mt (congr_arg g) ne
id           └┘  └───────┘   └┘
src    └────┘└┘ └───────┘ └┘└┘
typ    └────┘└┘ └───────┘└┘└┘
doc    └────┘             └┘  
txt    └────┘             └┘  
par    └────┘             └┘  
pid                      └┘  
st   ───────────────────────────┘
166  end
st   └─┘
167  
168  @[to_additive]
doc    └─────────┘
169  lemma prod_mul_distrib : s.prod (λx, f x * g x) = s.prod f * s.prod g :=
id                            └───┘            └───┘   └───┘ 
src                            └───┘                  └───┘     └───┘
typ                           └───┘            └───┘   └───┘ 
doc                            └───┘                    └───┘      └───┘
170  eq.trans (by rw one_mul; refl) fold_op_distrib
id   └──────┘        └─────┘        └─────────────┘
src  └──────┘     └─┘└─────┘  └──┘  └─────────────┘
typ  └──────┘     └─┘└─────┘  └──┘  └─────────────┘
doc               └─┘         └──┘
txt               └─┘         └──┘
par               └─┘         └──┘
pid                 
st               └───────────────┘
171  
172  @[to_additive]
doc    └─────────┘
173  lemma prod_comm [decidable_eq γ] {s : finset γ} {t : finset α} {f : γ → α → β} :
id                    └──────────┘        └────┘        └────┘              
src                   └──────────┘         └────┘         └────┘
typ                   └──────────┘        └────┘        └────┘              
doc                                        └────┘         └────┘
174    s.prod (λx, t.prod $ f x) = t.prod (λy, s.prod $ λx, f x y) :=
id     └───┘     └───┘       └───┘     └───┘        
src     └───┘       └───┘          └───┘       └───┘
typ    └───┘     └───┘       └───┘     └───┘        
doc     └───┘       └───┘           └───┘       └───┘
175  finset.induction_on s (by simp only [prod_empty, prod_const_one]) $
id   └─────────────────┘                 └────────┘  └────────────┘
src  └─────────────────┘       └─────────┘└────────┘└┘└────────────┘
typ  └─────────────────┘      └─────────┘└────────┘└┘└────────────┘
doc  └─────────────────┘       └─────────┘          └┘              
txt                            └─────────┘          └┘              
par                            └─────────┘          └┘              
pid                                └──┘└┘          └┘              
st                            └─────────────────────────────────────┘
176  λ _ _ H ih, by simp only [prod_insert H, prod_mul_distrib, ih]
id        └┘                └─────────┘   └──────────────┘  └┘
src                 └─────────┘└─────────┘ └┘└──────────────┘└┘  └─
typ       └┘     └─────────┘└─────────┘└┘└──────────────┘└┘└┘└─
doc                 └─────────┘            └┘                └┘  └─
txt                 └─────────┘            └┘                └┘  └─
par                 └─────────┘            └┘                └┘  └─
pid                     └──┘└┘            └┘                └┘  
st                 └────────────────────────────────────────────────
177  
src  
typ  
doc  
txt  
par  
pid  
st   
178  @[to_additive]
doc    └─────────┘
179  lemma prod_hom [comm_monoid γ] (s : finset α) {f : α → β} (g : β → γ) [is_monoid_hom g] :
id                   └─────────┘        └────┘                        └───────────┘ 
src                  └─────────┘         └────┘                             └───────────┘
typ                  └─────────┘        └────┘                        └───────────┘ 
doc                                      └────┘                             └───────────┘
180    s.prod (λx, g (f x)) = g (s.prod f) :=
id     └───┘              └───┘ 
src     └───┘                    └───┘
typ    └───┘              └───┘ 
doc     └───┘                     └───┘
181  by { delta finset.prod, rw [← multiset.map_map, multiset.prod_hom _ g] }
id                                 └──────────────┘  └───────────────┘   
src       └───────────────┘  └────┘└──────────────┘└┘└───────────────┘└─┘ └┘
typ       └───────────────┘  └────┘└──────────────┘└┘└───────────────┘└─┘└┘
doc       └───────────────┘  └────┘                └┘                 └─┘ └┘
txt       └───────────────┘  └────┘                └┘                 └─┘ └┘
par       └───────────────┘  └────┘                └┘                 └─┘ └┘
pid            └──────────┘    └──┘                └┘                 └─┘ 
st     └──────────────────┘└──────────────────────┘└─────────────────────┘└┘
182  
183  @[to_additive]
doc    └─────────┘
184  lemma prod_hom_rel [comm_monoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : finset α}
id                       └─────────┘                                             └────┘ 
src                      └─────────┘                                                    └────┘
typ                      └─────────┘                                             └────┘ 
doc                                                                                     └────┘
185    (h₁ : r 1 1) (h₂ : ∀a b c, r b c → r (f a * b) (g a * c)) : r (s.prod f) (s.prod g) :=
id                                                   └───┘    └───┘ 
src                                                                  └───┘      └───┘
typ                                                  └───┘    └───┘ 
doc                                                                    └───┘      └───┘
186  by { delta finset.prod, apply multiset.prod_hom_rel; assumption }
id                                 └───────────────────┘
src       └───────────────┘  └────┘└───────────────────┘  └─────────┘
typ       └───────────────┘  └────┘└───────────────────┘  └─────────┘
doc       └───────────────┘  └────┘                       └─────────┘
txt       └───────────────┘  └────┘                       └─────────┘
par       └───────────────┘  └────┘                       └─────────┘
pid            └──────────┘                                        
st     └──────────────────┘└────────────────────────────────────────┘└┘
187  
188  @[to_additive]
doc    └─────────┘
189  lemma prod_subset (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → f x = 1) : s₁.prod f = s₂.prod f :=
id                          └┘  └┘          └┘    └┘           └┘└───┘   └┘└───┘ 
src                                                                  └───┘      └───┘
typ                         └┘  └┘          └┘    └┘           └┘└───┘   └┘└───┘ 
doc                                                                     └───┘       └───┘
190  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
191  have (s₂ \ s₁).prod f = (s₂ \ s₁).prod (λx, 1),
id                         └┘   └┘
src           └─────┘       └─────┘  └──────
typ           └─────┘ └┘ └┘└─────┘  └──────
doc            └─────┘        └─────┘  └──────
txt            └─────┘        └─────┘  └──────
par            └─────┘        └─────┘  └──────
pid            └─────┘        └─────┘  └──────
st   ────────────────────────────────────────────────
192    from prod_congr rfl $ by simpa only [mem_sdiff, and_imp],
id          └────────┘ └─┘                  └───────┘  └─────┘
src  ──────┘└────────┘└─┘   └──────────┘└───────┘└┘└─────┘└┘
typ  ──────┘└────────┘└─┘   └──────────┘└───────┘└┘└─────┘└┘
doc  ──────┘                └──────────┘         └┘       └┘
txt  ──────┘                └──────────┘         └┘       └┘
par  ──────┘                └──────────┘         └┘       └┘
pid  ──────┘                └───────────┘         └┘       └─┘
st   ─────────────────────────┘└──────────────────────────────┘└─
193  by rw [←prod_sdiff h]; simp only [this, prod_const_one, one_mul]
id           └────────┘               └──┘  └────────────┘  └─────┘
src    └───┘└────────┘ └┘└─────────┘    └┘└────────────┘└┘└─────┘└─
typ    └───┘└────────┘└┘└─────────┘└──┘└┘└────────────┘└┘└─────┘└─
doc    └───┘           └┘└─────────┘    └┘              └┘       └─
txt    └───┘           └┘└─────────┘    └┘              └┘       └─
par    └───┘           └┘└─────────┘    └┘              └┘       └─
pid    └────┘           └────────────┘    └┘              └┘       └─
st   ─┘└────────────────┘└───────────────────────────────────────────
194  
src  
typ  
doc  
txt  
par  
pid  
st   
195  -- If we use `[decidable_eq β]` here, some rewrites fail because they find a wrong `decidable`
src  ───────────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────────
196  -- instance first; `{∀x, decidable (f x ≠ 1)}` doesn't work with `rw ← prod_filter_ne_one`
src  ──────────────────────────────────────────────────────────────────────────────────────────┘
typ  ──────────────────────────────────────────────────────────────────────────────────────────┘
doc  ──────────────────────────────────────────────────────────────────────────────────────────┘
txt  ──────────────────────────────────────────────────────────────────────────────────────────┘
par  ──────────────────────────────────────────────────────────────────────────────────────────┘
pid  ──────────────────────────────────────────────────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘
197  @[to_additive]
doc    └─────────┘
198  lemma prod_filter_ne_one [∀ x, decidable (f x ≠ 1)] : (s.filter $ λx, f x ≠ 1).prod f = s.prod f :=
id                                 └───────┘            └─────┘           └──┘    └───┘ 
src                                 └───────┘               └─────┘              └──┘      └───┘
typ                                └───────┘            └─────┘           └──┘    └───┘ 
doc                                                          └─────┘               └──┘       └───┘
199  prod_subset (filter_subset _) $ λ x,
id   └─────────┘  └───────────┘        
src  └─────────┘  └───────────┘
typ  └─────────┘  └───────────┘        
200    by { classical, rw [not_imp_comm, mem_filter], exact and.intro }
id                         └──────────┘  └────────┘         └───────┘
src         └───────┘  └──┘└──────────┘└┘└────────┘  └────┘└───────┘
typ         └───────┘  └──┘└──────────┘└┘└────────┘  └────┘└───────┘
doc         └───────┘  └──┘            └┘            └────┘         
txt         └───────┘  └──┘            └┘            └────┘         
par         └───────┘  └──┘            └┘            └────┘         
pid                      └┘            └┘                          
st       └──────────┘└────────────────┘└──────────┘└─────────────────┘└┘
201  
202  @[to_additive]
doc    └─────────┘
203  lemma prod_filter (p : α → Prop) [decidable_pred p] (f : α → β) :
id                                    └────────────┘           
src                                    └────────────┘
typ                                   └────────────┘           
204    (s.filter p).prod f = s.prod (λa, if p a then f a else 1) :=
id      └─────┘  └──┘    └───┘                
src      └─────┘   └──┘      └───┘
typ     └─────┘  └──┘    └───┘                
doc      └─────┘   └──┘       └───┘
205  calc (s.filter p).prod f = (s.filter p).prod (λa, if p a then f a else 1) :
id         └─────┘  └──┘      └─────┘  └──┘                 
src         └─────┘   └──┘        └─────┘   └──┘
typ        └─────┘  └──┘      └─────┘  └──┘                 
doc         └─────┘   └──┘        └─────┘   └──┘
206      prod_congr rfl (assume a h, by rw [if_pos (mem_filter.1 h).2])
id       └────────┘ └─┘                   └────┘  └────────┘   
src      └────────┘ └─┘                 └──┘└────┘ └────────┘└─┘ └──┘
typ      └────────┘ └─┘               └──┘└────┘ └────────┘└─┘└──┘
doc                                     └──┘                 └─┘ └──┘
txt                                     └──┘                 └─┘ └──┘
par                                     └──┘                 └─┘ └──┘
pid                                       └┘                 └─┘ └──┘
st                                     └──────────────────────────┘└─┘
207    ... = s.prod (λa, if p a then f a else 1) :
id           └───┘                
src           └───┘
typ          └───┘                
doc           └───┘
208      begin
st       └─────
209        refine prod_subset (filter_subset s) (assume x hs h, _),
id                └─────────┘  └───────────┘ 
src        └─────┘└─────────┘ └───────────┘ └┘       └─────────┘
typ        └─────┘└─────────┘ └───────────┘└┘       └─────────┘
doc        └─────┘                          └┘       └─────────┘
txt        └─────┘                          └┘       └─────────┘
par        └─────┘                          └┘       └─────────┘
pid                                        └┘       └─────────┘
st   ────────────────────────────────────────────────────────────┘└─
210        rw [mem_filter, not_and] at h,
id             └────────┘  └─────┘
src        └──┘└────────┘└┘└─────┘└────┘
typ        └──┘└────────┘└┘└─────┘└────┘
doc        └──┘          └┘       └────┘
txt        └──┘          └┘       └────┘
par        └──┘          └┘       └────┘
pid          └┘          └┘       └───┘
st   ───────────────────┘└───────┘└───┘└─
211        exact if_neg (h hs)
id               └────┘   └┘
src        └────┘└────┘    └─
typ        └────┘└────┘ └┘└─
doc        └────┘          └─
txt        └────┘          └─
par        └────┘          └─
pid                       
st   ──────────────────────────
212      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
213  
214  @[to_additive]
doc    └─────────┘
215  lemma prod_eq_single {s : finset α} {f : α → β} (a : α)
id                             └────┘                  
src                            └────┘
typ                            └────┘                  
doc                            └────┘
216    (h₀ : ∀b∈s, b ≠ a → f b = 1) (h₁ : a ∉ s → f a = 1) : s.prod f = f a :=
id                                             └───┘    
src                                                       └───┘   
typ                                            └───┘    
doc                                                           └───┘
217  by haveI := classical.dec_eq α;
id               └──────────────┘ 
src     └───────┘└──────────────┘
typ     └───────┘└──────────────┘
doc     └───────┘                
txt     └───────┘                
par     └───────┘                
pid          └─┘                
st     └─────────────────────────────
218  from classical.by_cases
id        └────────────────┘
src  └───┘└────────────────┘
typ  └───┘└────────────────┘
doc  └───┘                  
txt  └───┘                  
par  └───┘                  
pid  └───┘                  
st   ────────────────────────
219    (assume : a ∈ s,
id                 
src  ─┘       └─┘  └─
typ  ─┘       └─┘  └─
doc  ─┘       └─┘   └─
txt  ─┘       └─┘   └─
par  ─┘       └─┘   └─
pid  ─┘       └─┘   └─
st   ───────────────────
220      calc s.prod f = ({a} : finset α).prod f :
id            └────┘           └────┘ 
src  ───┘    └────┘   └───┘└────┘ └─────┘ └──
typ  ───┘    └────┘   └───┘└────┘└─────┘ └──
doc  ───┘    └────┘   └───┘└────┘ └─────┘ └──
txt  ───┘              └───┘       └─────┘ └──
par  ───┘              └───┘       └─────┘ └──
pid  ───┘              └───┘       └─────┘ └──
st   ──────────────────────────────────────────────
221        begin
src  ─────┘     
typ  ─────┘     
doc  ─────┘     
txt  ─────┘     
par  ─────┘     
pid  ─────┘     
st   ─────┘└─────
222          refine (prod_subset _ _).symm,
id                   └─────────┘
src  ───────┘└─────┘ └─────────┘└────────┘└─
typ  ──────────────┘ └─────────┘└───────────
doc  ───────┘└─────┘            └────────┘└─
txt  ───────┘└─────┘            └────────┘└─
par  ──────────────┘            └───────────
pid  ──────────────┘            └───────────
st   ────────────────────────────────────┘└─
223          { intros _ H, rwa mem_singleton.1 H },
id                             └───────────┘   
src  ─────────┘└────────┘└┘└──┘└───────────┘└─┘ └──
typ  ─────────┘└────────┘└┘└──┘└───────────┘└─┘└──
doc  ─────────┘└────────┘└┘└──┘             └─┘ └──
txt  ─────────┘└────────┘└┘└──┘             └─┘ └──
par  ─────────┘└────────┘└┘└──┘             └─┘ └──
pid  ─────────────────────────┘             └─┘ └───
st   ────────┘└─────────┘└──────────────────────┘└─
224          { simpa only [mem_singleton] }
id                         └───────────┘
src  ─────────┘└──────────┘└───────────┘└┘└─
typ  ─────────┘└──────────┘└───────────┘└┘└─
doc  ─────────┘└──────────┘             └┘└─
txt  ─────────┘└──────────┘             └┘└─
par  ─────────┘└──────────┘             └┘└─
pid  ─────────────────────┘             └───
st   ────────────────────────────────────┘└─
225        end
src  ──────────
typ  ──────────
doc  ──────────
txt  ──────────
par  ──────────
pid  ──────────
st   ────────┘
226        ... = f a : prod_singleton)
id                    └────────────┘
src  ─────────┘   └─┘└────────────┘└─
typ  ─────────┘  └─┘└────────────┘└─
doc  ─────────┘   └─┘              └─
txt  ─────────┘   └─┘              └─
par  ─────────┘   └─┘              └─
pid  ─────────┘   └─┘              └─
st   ──────────────────────────────────
227    (assume : a ∉ s,
id                 
src  ─┘       └─┘  └─
typ  ─┘       └─┘└─
doc  ─┘       └─┘   └─
txt  ─┘       └─┘   └─
par  ─┘       └─┘   └─
pid  ─┘       └─┘   └─
st   ───────────────────
228      (prod_congr rfl $ λ b hb, h₀ b hb $ by rintro rfl; cc).trans $
id        └────────┘ └─┘           └┘
src  ───┘ └────────┘└─┘  └─────┘        └────────┘└┘└┘└──────┘ 
typ  ───┘ └────────┘└─┘  └─────┘└┘      └────────┘└┘└┘└──────┘ 
doc  ───┘                └─────┘        └────────┘└┘└┘└──────┘ 
txt  ───┘                └─────┘        └────────┘└┘└┘└──────┘ 
par  ───┘                └─────┘        └────────┘└┘└┘└──────┘ 
pid  ───┘                └─────┘        └─────────────────────┘ 
st   ─────────────────────────────────────────┘└─────────────┘└─────────
229        prod_const_one.trans (h₁ this).symm)
id         └──────────────────┘  └┘
src  ─────┘└──────────────────┘       └───────
typ  ─────┘└──────────────────┘ └┘    └───────
doc  ─────┘                           └───────
txt  ─────┘                           └───────
par  ─────┘                           └───────
pid  ─────┘                           └─────┘
st   ───────────────────────────────────────────
230  
src  
typ  
doc  
txt  
par  
pid  
st   
231  @[to_additive] lemma prod_ite [comm_monoid γ] {s : finset α}
id                                  └─────────┘        └────┘ 
src                                 └─────────┘         └────┘
typ                                 └─────────┘        └────┘ 
doc    └─────────┘                                      └────┘
232    {p : α → Prop} {hp : decidable_pred p} (f g : α → γ) (h : γ → β) :
id                         └────────────┘                       
src                         └────────────┘
typ                        └────────────┘                       
233    s.prod (λ x, h (if p x then f x else g x)) =
id     └───┘                             
src     └───┘                                     
typ    └───┘                             
doc     └───┘
234    (s.filter p).prod (λ x, h (f x)) * (s.filter (λ x, ¬ p x)).prod (λ x, h (g x)) :=
id      └─────┘  └──┘               └─────┘          └──┘          
src      └─────┘   └──┘                    └─────┘             └──┘
typ     └─────┘  └──┘               └─────┘          └──┘          
doc      └─────┘   └──┘                     └─────┘              └──┘
235  by letI := classical.dec_eq α; exact
id              └──────────────┘ 
src     └──────┘└──────────────┘   └────┘
typ     └──────┘└──────────────┘  └────┘
doc     └──────┘                   └────┘
txt     └──────┘                   └────┘
par     └──────┘                   └────┘
pid         └─┘                        
st     └──────────────────────────────────
236  calc s.prod (λ x, h (if p x then f x else g x))
id        └────┘
src      └────┘  └──┘    └─┘ └────┘  └────┘  └──
typ      └────┘  └──┘    └─┘ └────┘  └────┘  └──
doc      └────┘  └──┘    └─┘ └────┘  └────┘  └──
txt              └──┘    └─┘ └────┘  └────┘  └──
par              └──┘    └─┘ └────┘  └────┘  └──
pid              └──┘    └─┘ └────┘  └────┘  └──
st   ────────────────────────────────────────────────
237      = (s.filter p ∪ s.filter (λ x, ¬ p x)).prod (λ x, h (if p x then f x else g x)) :
id                      └──────┘                                                
src  ───┘           └──────┘  └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
typ  ───┘           └──────┘  └──┘   └──────┘  └──┘   └─┘ └────┘ └────┘ └────
doc  ───┘            └──────┘  └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
txt  ───┘                      └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
par  ───┘                      └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
pid  ───┘                      └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
st   ──────────────────────────────────────────────────────────────────────────────────────
238    by rw [filter_union_filter_neg_eq]
id            └────────────────────────┘
src  ─┘  └──┘└────────────────────────┘└┘
typ  ─┘  └──┘└────────────────────────┘└┘
doc  ─┘  └──┘                          └┘
txt  ─┘  └──┘                          └┘
par  ─┘  └──┘                          └┘
pid  ─┘  └───┘                          └─
st   ───┘└─────────────────────────────┘
239  ... = (s.filter p).prod (λ x, h (if p x then f x else g x)) *
id                                                               
src  └──┘           └─────┘  └──┘    └─┘ └────┘  └────┘  └─┘
typ  └──┘           └─────┘  └──┘    └─┘ └────┘  └────┘  └─┘
doc  └──┘           └─────┘  └──┘    └─┘ └────┘  └────┘  └─┘ 
txt  └──┘           └─────┘  └──┘    └─┘ └────┘  └────┘  └─┘ 
par  └──┘           └─────┘  └──┘    └─┘ └────┘  └────┘  └─┘ 
pid  ───┘           └─────┘  └──┘    └─┘ └────┘  └────┘  └─┘ 
st   └─────────────────────────────────────────────────────────────
240      (s.filter (λ x, ¬ p x)).prod (λ x, h (if p x then f x else g x)) :
src  ───┘           └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
typ  ───┘           └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
doc  ───┘           └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
txt  ───┘           └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
par  ───┘           └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
pid  ───┘           └──┘   └──────┘  └──┘    └─┘ └────┘  └────┘  └────
st   ───────────────────────────────────────────────────────────────────────
241    prod_union (by simp [disjoint_right] {contextual := tt})
id     └────────┘           └────────────┘                 └┘
src  ─┘└────────┘   └────┘└────────────┘└┘ └────────────┘└┘└─
typ  ─┘└────────┘   └────┘└────────────┘└┘ └────────────┘└┘└─
doc  ─┘             └────┘              └┘ └────────────┘  └─
txt  ─┘             └────┘              └┘ └────────────┘  └─
par  ─┘             └────┘              └┘ └────────────┘  └─
pid  ─┘             └─────┘              └┘ └────────────┘  └──
st   ───────────────┘└───────────────────────────────────────┘└─
242  ... = (s.filter p).prod (λ x, h (f x)) * (s.filter (λ x, ¬ p x)).prod (λ x, h (g x)) :
src  ───┘           └─────┘  └──┘    └─┘            └──┘   └──────┘  └──┘    └────
typ  ───┘           └─────┘  └──┘    └─┘            └──┘   └──────┘  └──┘    └────
doc  ───┘           └─────┘  └──┘    └─┘            └──┘   └──────┘  └──┘    └────
txt  ───┘           └─────┘  └──┘    └─┘            └──┘   └──────┘  └──┘    └────
par  ───┘           └─────┘  └──┘    └─┘            └──┘   └──────┘  └──┘    └────
pid  ───┘           └─────┘  └──┘    └─┘            └──┘   └──────┘  └──┘    └────
st   ───────────────────────────────────────────────────────────────────────────────────────
243    congr_arg2 _
id     └────────┘
src  ─┘└────────┘└──
typ  ─┘└────────┘└──
doc  ─┘          └──
txt  ─┘          └──
par  ─┘          └──
pid  ─┘          └──
st   ───────────────
244      (prod_congr rfl (by simp {contextual := tt}))
id                                               └┘
src  ───┘                 └───┘ └────────────┘└┘└──
typ  ───┘                 └───┘ └────────────┘└┘└──
doc  ───┘                 └───┘ └────────────┘  └──
txt  ───┘                 └───┘ └────────────┘  └──
par  ───┘                 └───┘ └────────────┘  └──
pid  ───┘                 └────┘ └────────────┘  └───
st   ──────────────────────┘└──────────────────────┘└──
245      (prod_congr rfl (by simp {contextual := tt}))
id        └────────┘ └─┘                         └┘
src  ───┘ └────────┘└─┘   └───┘ └────────────┘└┘└──
typ  ───┘ └────────┘└─┘   └───┘ └────────────┘└┘└──
doc  ───┘                 └───┘ └────────────┘  └──
txt  ───┘                 └───┘ └────────────┘  └──
par  ───┘                 └───┘ └────────────┘  └──
pid  ───┘                 └────┘ └────────────┘  └─┘
st   ──────────────────────┘└──────────────────────┘└──
246  
src  
typ  
doc  
txt  
par  
pid  
st   
247  @[simp, to_additive] lemma prod_ite_eq [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
id                                           └──────────┘        └────┘                  
src                                          └──────────┘         └────┘
typ                                          └──────────┘        └────┘                  
doc    └──┘  └─────────┘                                          └────┘
248    s.prod (λ x, (ite (a = x) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
id     └───┘       └─┘               └─┘        
src     └───┘        └─┘                   └─┘    
typ    └───┘       └─┘               └─┘        
doc     └───┘
249  begin
st   └─────
250    rw ←finset.prod_filter,
id         └────────────────┘
src    └──┘└────────────────┘
typ    └──┘└────────────────┘
doc    └──┘
txt    └──┘
par    └──┘
pid      └┘
st   ───────────────────────┘└─
251    split_ifs;
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ─────────────
252    simp only [filter_eq, if_true, if_false, h, prod_empty, prod_singleton, insert_empty_eq_singleton],
id                └───────┘  └─────┘  └──────┘    └────────┘  └────────────┘  └───────────────────────┘
src    └─────────┘└───────┘└┘└─────┘└┘└──────┘└┘ └┘└────────┘└┘└────────────┘└┘└───────────────────────┘
typ    └─────────┘└───────┘└┘└─────┘└┘└──────┘└┘└┘└────────┘└┘└────────────┘└┘└───────────────────────┘
doc    └─────────┘└───────┘└┘       └┘        └┘ └┘          └┘              └┘                         
txt    └─────────┘         └┘       └┘        └┘ └┘          └┘              └┘                         
par    └─────────┘         └┘       └┘        └┘ └┘          └┘              └┘                         
pid        └──┘└┘         └┘       └┘        └┘ └┘          └┘              └┘                         
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
253  end
st   ──┘
254  
255  /--
256    When a product is taken over a conditional whose condition is an equality test on the index
257    and whose alternative is 1, then the product's value is either the term at that index or `1`.
258  
259    The difference with `prod_ite_eq` is that the arguments to `eq` are swapped.
260  -/
261  @[simp, to_additive] lemma prod_ite_eq' [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
id                                            └──────────┘        └────┘                  
src                                           └──────────┘         └────┘
typ                                           └──────────┘        └────┘                  
doc    └──┘  └─────────┘                                           └────┘
262    s.prod (λ x, (ite (x = a) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
id     └───┘       └─┘               └─┘        
src     └───┘        └─┘                   └─┘    
typ    └───┘       └─┘               └─┘        
doc     └───┘
263  begin
st   └─────
264    rw ←prod_ite_eq,
id         └─────────┘
src    └──┘└─────────┘
typ    └──┘└─────────┘
doc    └──┘
txt    └──┘
par    └──┘
pid      └┘
st   ────────────────┘└─
265    congr, ext x,
src    └───┘  └───┘
typ    └───┘  └───┘
doc           └───┘
txt    └───┘  └───┘
par    └───┘  └───┘
pid              └┘
st   ──────┘└─────┘└─
266    by_cases x = a; finish
id                
src    └───────┘    └─────┘
typ    └───────┘  └─────┘
doc    └───────┘     └─────┘
txt    └───────┘     └─────┘
par    └───────┘     └─────┘
pid                       
st   ────────────────────────┘
267  end
st   └─┘
268  
269  @[to_additive]
doc    └─────────┘
270  lemma prod_attach {f : α → β} : s.attach.prod (λx, f x.val) = s.prod f :=
id                                 └─────┘└───┘      └──┘   └───┘ 
src                                   └─────┘└───┘         └──┘    └───┘
typ                                └─────┘└───┘      └──┘   └───┘ 
doc                                   └─────┘└───┘                  └───┘
271  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
272  calc s.attach.prod (λx, f x.val) = ((s.attach).image subtype.val).prod f :
id        └───────────┘         └──┘      └──────┘        └─────────┘       
src      └───────────┘  └─┘  └──┘└┘   └──────┘└──────┘└─────────┘└─────┘ └──
typ      └───────────┘  └─┘  └──┘└┘   └──────┘└──────┘└─────────┘└─────┘└──
doc      └───────────┘  └─┘      └┘   └──────┘└──────┘           └─────┘ └──
txt                     └─┘      └┘           └──────┘           └─────┘ └──
par                     └─┘      └┘           └──────┘           └─────┘ └──
pid                     └─┘      └┘           └──────┘           └─────┘ └──
st   ───────────────────────────────────────────────────────────────────────────
273      by rw [prod_image]; exact assume x _ y _, subtype.eq
id              └────────┘                         └────────┘
src  ───┘  └──┘└────────┘└──────┘      └────────┘└────────┘
typ  ───┘  └──┘└────────┘└──────┘      └────────┘└────────┘
doc  ───┘  └──┘          └──────┘      └────────┘          
txt  ───┘  └──┘          └──────┘      └────────┘          
par  ───┘  └──┘          └──────┘      └────────┘          
pid  ───┘  └───┘          └───────┘      └────────┘          
st   ─────┘└─────────────┘└──────────────────────────────────
274    ... = _ : by rw [attach_image_val]
id                      └──────────────┘
src  ─────┘ └───┘  └──┘└──────────────┘└─
typ  ─────┘ └───┘  └──┘└──────────────┘└─
doc  ─────┘ └───┘  └──┘                └─
txt  ─────┘ └───┘  └──┘                └─
par  ─────┘ └───┘  └──┘                └─
pid  ─────┘ └───┘  └───┘                └─
st   ─┘└──────────┘└───────────────────┘
275  
src  
typ  
doc  
txt  
par  
pid  
st   
276  @[to_additive]
doc    └─────────┘
277  lemma prod_bij {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
id                       └────┘        └────┘                     
src                      └────┘         └────┘
typ                      └────┘        └────┘                     
doc                      └────┘         └────┘
278    (i : Πa∈s, γ) (hi : ∀a ha, i a ha ∈ t) (h : ∀a ha, f a = g (i a ha))
id                        └┘    └┘           └┘         └┘
src                                                          
typ                       └┘    └┘           └┘         └┘
279    (i_inj : ∀a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀b∈t, ∃a ha, b = i a ha) :
id               └┘ └┘ └─┘ └─┘   └┘ └─┘   └┘ └─┘   └┘  └┘                 └┘     └┘
src                                                                                 
typ              └┘ └┘ └─┘ └─┘   └┘ └─┘   └┘ └─┘   └┘  └┘                 └┘     └┘
280    s.prod f = t.prod g :=
id     └───┘   └───┘ 
src     └───┘     └───┘
typ    └───┘   └───┘ 
doc     └───┘      └───┘
281  congr_arg multiset.prod
id   └───────┘ └───────────┘
src  └───────┘ └───────────┘
typ  └───────┘ └───────────┘
doc            └───────────┘
282    (multiset.map_eq_map_of_bij_of_nodup f g s.2 t.2 i hi h i_inj i_surj)
id      └─────────────────────────────────┘        └┘  └───┘ └────┘
src     └─────────────────────────────────┘         
typ     └─────────────────────────────────┘        └┘  └───┘ └────┘
283  
284  @[to_additive]
doc    └─────────┘
285  lemma prod_bij_ne_one {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
id                              └────┘        └────┘                     
src                             └────┘         └────┘
typ                             └────┘        └────┘                     
doc                             └────┘         └────┘
286    (i : Πa∈s, f a ≠ 1 → γ) (hi₁ : ∀a h₁ h₂, i a h₁ h₂ ∈ t)
id                                └┘ └┘    └┘ └┘  
src                                                      
typ                               └┘ └┘    └┘ └┘  
287    (hi₂ : ∀a₁ a₂ h₁₁ h₁₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
id             └┘ └┘ └─┘ └─┘ └─┘ └─┘   └┘ └─┘ └─┘   └┘ └─┘ └─┘   └┘  └┘
src                                                                   
typ            └┘ └┘ └─┘ └─┘ └─┘ └─┘   └┘ └─┘ └─┘   └┘ └─┘ └─┘   └┘  └┘
288    (hi₃ : ∀b∈t, g b ≠ 1 → ∃a h₁ h₂, b = i a h₁ h₂)
id                        └┘ └┘     └┘ └┘
src                                    
typ                       └┘ └┘     └┘ └┘
289    (h : ∀a h₁ h₂, f a = g (i a h₁ h₂)) :
id            └┘ └┘         └┘ └┘
src                       
typ           └┘ └┘         └┘ └┘
290    s.prod f = t.prod g :=
id     └───┘   └───┘ 
src     └───┘     └───┘
typ    └───┘   └───┘ 
doc     └───┘      └───┘
291  by classical; exact
src     └───────┘  └────┘
typ     └───────┘  └────┘
doc     └───────┘  └────┘
txt     └───────┘  └────┘
par     └───────┘  └────┘
pid                     
st     └─────────────────
292  calc s.prod f = (s.filter $ λx, f x ≠ 1).prod f : prod_filter_ne_one.symm
id        └────┘      └──────┘                        └─────────────────────┘
src      └────┘   └──────┘  └─┘   └───────┘ └─┘└─────────────────────┘
typ      └────┘   └──────┘  └─┘   └───────┘└─┘└─────────────────────┘
doc      └────┘   └──────┘  └─┘   └───────┘ └─┘                       
txt                         └─┘   └───────┘ └─┘                       
par                         └─┘   └───────┘ └─┘                       
pid                         └─┘   └───────┘ └─┘                       
st   ──────────────────────────────────────────────────────────────────────────
293    ... = (t.filter $ λx, g x ≠ 1).prod g :
id            └──────┘           
src  ─────┘  └──────┘  └─┘  └───────┘ └──
typ  ─────┘  └──────┘  └─┘  └───────┘ └──
doc  ─────┘  └──────┘  └─┘   └───────┘ └──
txt  ─────┘            └─┘   └───────┘ └──
par  ─────┘            └─┘   └───────┘ └──
pid  ─────┘            └─┘   └───────┘ └──
st   ──────────────────────────────────────────
294      prod_bij (assume a ha, i a (mem_filter.mp ha).1 (mem_filter.mp ha).2)
id       └──────┘               
src  ───┘└──────┘       └─────┘                  └──┘                └────
typ  ───┘└──────┘       └─────┘                 └──┘                └────
doc  ───┘               └─────┘                  └──┘                └────
txt  ───┘               └─────┘                  └──┘                └────
par  ───┘               └─────┘                  └──┘                └────
pid  ───┘               └─────┘                  └──┘                └────
st   ──────────────────────────────────────────────────────────────────────────
295        (assume a ha, (mem_filter.mp ha).elim $ λh₁ h₂, mem_filter.mpr
src  ─────┘       └─────┘                └─────┘  └─────┘              
typ  ─────┘       └─────┘                └─────┘  └─────┘              
doc  ─────┘       └─────┘                └─────┘  └─────┘              
txt  ─────┘       └─────┘                └─────┘  └─────┘              
par  ─────┘       └─────┘                └─────┘  └─────┘              
pid  ─────┘       └─────┘                └─────┘  └─────┘              
st   ─────────────────────────────────────────────────────────────────────
296          ⟨hi₁ a h₁ h₂, λ hg, h₂ (hg ▸ h a h₁ h₂)⟩)
id            └─┘                       
src  ───────┘         └┘ └───┘           └───
typ  ───────┘ └─┘     └┘ └───┘           └───
doc  ───────┘         └┘ └───┘            └───
txt  ───────┘         └┘ └───┘            └───
par  ───────┘         └┘ └───┘            └───
pid  ───────┘         └┘ └───┘            └───
st   ──────────────────────────────────────────────────
297        (assume a ha, (mem_filter.mp ha).elim $ h a)
id                                                 
src  ─────┘       └─────┘                └─────┘   └─
typ  ─────┘       └─────┘                └─────┘  └─
doc  ─────┘       └─────┘                └─────┘   └─
txt  ─────┘       └─────┘                └─────┘   └─
par  ─────┘       └─────┘                └─────┘   └─
pid  ─────┘       └─────┘                └─────┘   └─
st   ───────────────────────────────────────────────────
298        (assume a₁ a₂ ha₁ ha₂,
src  ─────┘       └───────────────
typ  ─────┘       └───────────────
doc  ─────┘       └───────────────
txt  ─────┘       └───────────────
par  ─────┘       └───────────────
pid  ─────┘       └───────────────
st   ─────────────────────────────
299          (mem_filter.mp ha₁).elim $ λha₁₁ ha₁₂, (mem_filter.mp ha₂).elim $ λha₂₁ ha₂₂, hi₂ a₁ a₂ _ _ _ _)
id                                                                                         └─┘
src  ───────┘                 └─────┘  └─────────┘                 └─────┘  └─────────┘       └─────────
typ  ───────┘                 └─────┘  └─────────┘                 └─────┘  └─────────┘└─┘    └─────────
doc  ───────┘                 └─────┘  └─────────┘                 └─────┘  └─────────┘       └─────────
txt  ───────┘                 └─────┘  └─────────┘                 └─────┘  └─────────┘       └─────────
par  ───────┘                 └─────┘  └─────────┘                 └─────┘  └─────────┘       └─────────
pid  ───────┘                 └─────┘  └─────────┘                 └─────┘  └─────────┘       └─────────
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────
300        (assume b hb, (mem_filter.mp hb).elim $ λh₁ h₂,
id                        └───────────┘
src  ─────┘       └─────┘ └───────────┘  └─────┘  └──────
typ  ─────┘       └─────┘ └───────────┘  └─────┘  └──────
doc  ─────┘       └─────┘                └─────┘  └──────
txt  ─────┘       └─────┘                └─────┘  └──────
par  ─────┘       └─────┘                └─────┘  └──────
pid  ─────┘       └─────┘                └─────┘  └──────
st   ──────────────────────────────────────────────────────
301          let ⟨a, ha₁, ha₂, eq⟩ := hi₃ b h₁ h₂ in ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩)
id                  └─┘  └─┘  └┘     └─┘                └────────────┘
src  ───────┘     └┘   └┘   └┘└┘└───┘        └──┘  └┘└────────────┘    └┘   └─┘  └──
typ  ───────┘    └┘└─┘└┘└─┘└┘└┘└───┘└─┘     └──┘  └┘└────────────┘    └┘   └─┘  └──
doc  ───────┘     └┘   └┘   └┘  └───┘        └──┘  └┘                  └┘   └─┘  └──
txt  ───────┘     └┘   └┘   └┘  └───┘        └──┘  └┘                  └┘   └─┘  └──
par  ───────┘     └┘   └┘   └┘  └───┘        └──┘  └┘                  └┘   └─┘  └──
pid  ───────┘     └┘   └┘   └┘  └───┘        └──┘  └┘                  └┘   └─┘  └──
st   ────────────────────────────────────────────────────────────────────────────────────
302    ... = t.prod g : prod_filter_ne_one
id           └────┘    └────────────────┘
src  ─────┘ └────┘ └─┘└────────────────┘
typ  ─────┘ └────┘└─┘└────────────────┘
doc  ─────┘ └────┘ └─┘                  
txt  ─────┘        └─┘                  
par  ─────┘        └─┘                  
pid  ─────┘        └─┘                  
st   ──────────────────────────────────────
303  
src  
typ  
doc  
txt  
par  
pid  
st   
304  @[to_additive]
doc    └─────────┘
305  lemma nonempty_of_prod_ne_one (h : s.prod f ≠ 1) : s.nonempty :=
id                                      └───┘        └───────┘
src                                      └───┘          └───────┘
typ                                     └───┘        └───────┘
doc                                      └───┘           └───────┘
306  s.eq_empty_or_nonempty.elim (λ H, false.elim $ h $ H.symm ▸ prod_empty) id
id   └───────────────────┘└───┘      └────────┘      └───┘  └────────┘  └┘
src   └───────────────────┘└───┘       └────────┘        └───┘  └────────┘  └┘
typ  └───────────────────┘└───┘      └────────┘      └───┘  └────────┘  └┘
307  
308  @[to_additive]
doc    └─────────┘
309  lemma exists_ne_one_of_prod_ne_one (h : s.prod f ≠ 1) : ∃a∈s, f a ≠ 1 :=
id                                           └───┘            
src                                           └───┘                 
typ                                          └───┘            
doc                                           └───┘
310  begin
st   └─────
311    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
312    rw ← prod_filter_ne_one at h,
id          └────────────────┘
src    └───┘└────────────────┘└───┘
typ    └───┘└────────────────┘└───┘
doc    └───┘                  └───┘
txt    └───┘                  └───┘
par    └───┘                  └───┘
pid      └─┘                  └───┘
st   ─────────────────────────────┘└─
313    rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩,
id            └─────────────────────┘ 
src    └─────┘└─────────────────────┘ └───────────┘
typ    └─────┘└─────────────────────┘└───────────┘
doc    └─────┘                        └───────────┘
txt    └─────┘                        └───────────┘
par    └─────┘                        └───────────┘
pid                                  └───────────┘
st   ──────────────────────────────────────────────┘└─
314    exact ⟨x, (mem_filter.1 hx).1, (mem_filter.1 hx).2⟩
id                                    └────────┘   └┘
src    └────┘  └┘           └─┘  └───┘ └────────┘└─┘  └───┘
typ    └────┘ └┘           └─┘  └───┘ └────────┘└─┘└┘└───┘
doc    └────┘  └┘           └─┘  └───┘           └─┘  └───┘
txt    └────┘  └┘           └─┘  └───┘           └─┘  └───┘
par    └────┘  └┘           └─┘  └───┘           └─┘  └───┘
pid           └┘           └─┘  └───┘           └─┘  └──┘
st   ─────────────────────────────────────────────────────┘
315  end
st   └─┘
316  
317  @[to_additive]
doc    └─────────┘
318  lemma prod_range_succ (f : ℕ → β) (n : ℕ) :
id                                        
src                                        
typ                                       
319    (range (nat.succ n)).prod f = f n * (range n).prod f :=
id      └───┘  └──────┘   └──┘        └───┘  └──┘  
src     └───┘  └──────┘    └──┘           └───┘   └──┘
typ     └───┘  └──────┘   └──┘        └───┘  └──┘  
doc     └───┘              └──┘             └───┘   └──┘
320  by rw [range_succ, prod_insert not_mem_range_self]
id          └────────┘  └─────────┘ └────────────────┘
src     └──┘└────────┘└┘└─────────┘└────────────────┘└─
typ     └──┘└────────┘└┘└─────────┘└────────────────┘└─
doc     └──┘          └┘                             └─
txt     └──┘          └┘                             └─
par     └──┘          └┘                             └─
pid       └┘          └┘                             
st     └─────────────┘└──────────────────────────────┘
321  
src  
typ  
doc  
txt  
par  
pid  
st   
322  lemma prod_range_succ' (f : ℕ → β) :
id                                  
src                              
typ                                 
323    ∀ n : ℕ, (range (nat.succ n)).prod f = (range n).prod (f ∘ nat.succ) * f 0
id             └───┘  └──────┘   └──┘     └───┘  └──┘     └──────┘   
src             └───┘  └──────┘    └──┘      └───┘   └──┘      └──────┘  
typ            └───┘  └──────┘   └──┘     └───┘  └──┘     └──────┘   
doc              └───┘              └──┘       └───┘   └──┘
324  | 0       := (prod_range_succ _ _).trans $ mul_comm _ _
id                 └─────────────┘     └───┘    └──────┘
src                └─────────────┘     └───┘    └──────┘
typ                └─────────────┘     └───┘    └──────┘
325  | (n + 1) := by rw [prod_range_succ (λ m, f (nat.succ m)), mul_assoc, ← prod_range_succ'];
id                      └─────────────┘         └──────┘      └───────┘    └──────────────┘
src                 └──┘└─────────────┘  └──┘  └──────┘ └──┘└───────┘└──┘                
typ                 └──┘└─────────────┘  └──┘ └──────┘ └──┘└───────┘└──┘└──────────────┘
doc                  └──┘                 └──┘           └──┘         └──┘                
txt                  └──┘                 └──┘           └──┘         └──┘                
par                  └──┘                 └──┘           └──┘         └──┘                
pid                    └┘                 └──┘           └──┘         └──┘                
st                  └────────────────────────────────────────┘└─────────┘└──────────────────┘└─
326                   exact prod_range_succ _ _
id                          └─────────────┘
src                   └────┘└─────────────┘└────
typ                   └────┘└─────────────┘└────
doc                   └────┘               └────
txt                   └────┘               └────
par                   └────┘               └────
pid                                       └──┘
st   ───────────────────────────────────────────
327  
src  
typ  
doc  
txt  
par  
pid  
st   
328  lemma sum_Ico_add {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (m n k : ℕ) :
id                                  └─────────────┘                      
src                                 └─────────────┘                        
typ                                 └─────────────┘                      
329    (Ico m n).sum (λ l, f (k + l)) = (Ico (m + k) (n + k)).sum f :=
id      └─┘   └─┘                └─┘           └─┘  
src     └─┘     └─┘                    └─┘               └─┘
typ     └─┘   └─┘                └─┘           └─┘  
doc     └─┘                              └─┘
330  Ico.image_add m n k ▸ eq.symm $ sum_image $ λ x hx y hy h, nat.add_left_cancel h
id   └───────────┘     └─────┘   └───────┘      └┘  └┘   └─────────────────┘ 
src  └───────────┘        └─────┘   └───────┘                  └─────────────────┘
typ  └───────────┘     └─────┘   └───────┘      └┘  └┘   └─────────────────┘ 
331  
332  @[to_additive]
doc    └─────────┘
333  lemma prod_Ico_add (f : ℕ → β) (m n k : ℕ) :
id                                         
src                                         
typ                                        
334    (Ico m n).prod (λ l, f (k + l)) = (Ico (m + k) (n + k)).prod f :=
id      └─┘   └──┘                └─┘           └──┘  
src     └─┘     └──┘                    └─┘               └──┘
typ     └─┘   └──┘                └─┘           └──┘  
doc     └─┘     └──┘                      └─┘                 └──┘
335  Ico.image_add m n k ▸ eq.symm $ prod_image $ λ x hx y hy h, nat.add_left_cancel h
id   └───────────┘     └─────┘   └────────┘      └┘  └┘   └─────────────────┘ 
src  └───────────┘        └─────┘   └────────┘                  └─────────────────┘
typ  └───────────┘     └─────┘   └────────┘      └┘  └┘   └─────────────────┘ 
336  
337  lemma sum_Ico_succ_top {δ : Type*} [add_comm_monoid δ] {a b : ℕ}
id                                       └─────────────┘          
src                                      └─────────────┘           
typ                                      └─────────────┘          
338    (hab : a ≤ b) (f : ℕ → δ) : (Ico a (b + 1)).sum f = (Ico a b).sum f + f b :=
id                             └─┘        └─┘     └─┘   └─┘     
src                               └─┘          └─┘      └─┘     └─┘    
typ                            └─┘        └─┘     └─┘   └─┘     
doc                                 └─┘                     └─┘
339  by rw [Ico.succ_top hab, sum_insert Ico.not_mem_top, add_comm]
id          └──────────┘ └─┘  └────────┘ └─────────────┘  └──────┘
src     └──┘└──────────┘   └┘└────────┘└─────────────┘└┘└──────┘└─
typ     └──┘└──────────┘└─┘└┘└────────┘└─────────────┘└┘└──────┘└─
doc     └──┘               └┘                         └┘        └─
txt     └──┘               └┘                         └┘        └─
par     └──┘               └┘                         └┘        └─
pid       └┘               └┘                         └┘        
st     └───────────────────┘└──────────────────────────┘└────────┘
340  
src  
typ  
doc  
txt  
par  
pid  
st   
341  @[to_additive]
doc    └─────────┘
342  lemma prod_Ico_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → β) :
id                                                       
src                                                     
typ                                                      
343    (Ico a b.succ).prod f = (Ico a b).prod f * f b :=
id      └─┘  └───┘ └──┘     └─┘   └──┘     
src     └─┘    └───┘ └──┘      └─┘     └──┘    
typ     └─┘  └───┘ └──┘     └─┘   └──┘     
doc     └─┘          └──┘       └─┘     └──┘
344  @sum_Ico_succ_top (additive β) _ _ _ hab _
id    └──────────────┘  └──────┘         └─┘
src   └──────────────┘  └──────┘
typ   └──────────────┘  └──────┘         └─┘
345  
346  lemma sum_eq_sum_Ico_succ_bot {δ : Type*} [add_comm_monoid δ] {a b : ℕ}
id                                              └─────────────┘          
src                                             └─────────────┘           
typ                                             └─────────────┘          
347    (hab : a < b) (f : ℕ → δ) : (Ico a b).sum f = f a + (Ico (a + 1) b).sum f :=
id                             └─┘   └─┘        └─┘        └─┘  
src                               └─┘     └─┘           └─┘          └─┘
typ                            └─┘   └─┘        └─┘        └─┘  
doc                                 └─┘                     └─┘
348  have ha : a ∉ Ico (a + 1) b, by simp,
id               └─┘       
src               └─┘              └──┘
typ              └─┘            └──┘
doc                └─┘               └──┘
txt                                  └──┘
par                                  └──┘
st                                  └───┘
349  by rw [← sum_insert ha, Ico.insert_succ_bot hab]
id            └────────┘ └┘  └─────────────────┘ └─┘
src     └────┘└────────┘  └┘└─────────────────┘   └─
typ     └────┘└────────┘└┘└┘└─────────────────┘└─┘└─
doc     └────┘            └┘                      └─
txt     └────┘            └┘                      └─
par     └────┘            └┘                      └─
pid       └──┘            └┘                      
st     └──────────────────┘└───────────────────────┘
350  
src  
typ  
doc  
txt  
par  
pid  
st   
351  @[to_additive]
doc    └─────────┘
352  lemma prod_eq_prod_Ico_succ_bot {a b : ℕ} (hab : a < b) (f : ℕ → β) :
id                                                               
src                                                             
typ                                                              
353    (Ico a b).prod f = f a * (Ico (a + 1) b).prod f :=
id      └─┘   └──┘        └─┘        └──┘  
src     └─┘     └──┘           └─┘          └──┘
typ     └─┘   └──┘        └─┘        └──┘  
doc     └─┘     └──┘             └─┘           └──┘
354  @sum_eq_sum_Ico_succ_bot (additive β) _ _ _ hab _
id    └─────────────────────┘  └──────┘         └─┘
src   └─────────────────────┘  └──────┘
typ   └─────────────────────┘  └──────┘         └─┘
355  
356  @[to_additive]
doc    └─────────┘
357  lemma prod_Ico_consecutive (f : ℕ → β) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
id                                                                       
src                                                                         
typ                                                                      
358    (Ico m n).prod f * (Ico n k).prod f = (Ico m k).prod f :=
id      └─┘   └──┘     └─┘   └──┘     └─┘   └──┘  
src     └─┘     └──┘      └─┘     └──┘      └─┘     └──┘
typ     └─┘   └──┘     └─┘   └──┘     └─┘   └──┘  
doc     └─┘     └──┘       └─┘     └──┘       └─┘     └──┘
359  Ico.union_consecutive hmn hnk ▸ eq.symm $ prod_union $ Ico.disjoint_consecutive m n k
id   └───────────────────┘ └─┘ └─┘  └─────┘   └────────┘   └──────────────────────┘   
src  └───────────────────┘          └─────┘   └────────┘   └──────────────────────┘
typ  └───────────────────┘ └─┘ └─┘  └─────┘   └────────┘   └──────────────────────┘   
360  
361  @[to_additive]
doc    └─────────┘
362  lemma prod_range_mul_prod_Ico (f : ℕ → β) {m n : ℕ} (h : m ≤ n) :
id                                                           
src                                                           
typ                                                          
363    (range m).prod f * (Ico m n).prod f = (range n).prod f :=
id      └───┘  └──┘     └─┘   └──┘     └───┘  └──┘  
src     └───┘   └──┘      └─┘     └──┘      └───┘   └──┘
typ     └───┘  └──┘     └─┘   └──┘     └───┘  └──┘  
doc     └───┘   └──┘       └─┘     └──┘       └───┘   └──┘
364  Ico.zero_bot m ▸ Ico.zero_bot n ▸ prod_Ico_consecutive f (nat.zero_le m) h
id   └──────────┘   └──────────┘   └──────────────────┘   └─────────┘   
src  └──────────┘    └──────────┘    └──────────────────┘    └─────────┘
typ  └──────────┘   └──────────┘   └──────────────────┘   └─────────┘   
365  
366  @[to_additive sum_Ico_eq_add_neg]
doc    └─────────┘
367  lemma prod_Ico_eq_div {δ : Type*} [comm_group δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
id                                      └────────┘                             
src                                     └────────┘                               
typ                                     └────────┘                             
368    (Ico m n).prod f = (range n).prod f * ((range m).prod f)⁻¹ :=
id      └─┘   └──┘     └───┘  └──┘      └───┘  └──┘   └┘
src     └─┘     └──┘      └───┘   └──┘       └───┘   └──┘    └┘
typ     └─┘   └──┘     └───┘  └──┘      └───┘  └──┘   └┘
doc     └─┘     └──┘       └───┘   └──┘        └───┘   └──┘
369  eq_mul_inv_iff_mul_eq.2 $ by rw [mul_comm]; exact prod_range_mul_prod_Ico f h
id   └───────────────────┘           └──────┘         └─────────────────────┘  
src  └───────────────────┘       └──┘└──────┘  └────┘└─────────────────────┘  
typ  └───────────────────┘       └──┘└──────┘  └────┘└─────────────────────┘
doc                               └──┘          └────┘                         
txt                               └──┘          └────┘                         
par                               └──┘          └────┘                         
pid                                 └┘                                        
st                               └───────────┘└───────────────────────────────────
370  
src  
typ  
doc  
txt  
par  
pid  
st   
371  lemma sum_Ico_eq_sub {δ : Type*} [add_comm_group δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
id                                     └────────────┘                             
src                                    └────────────┘                               
typ                                    └────────────┘                             
372    (Ico m n).sum f = (range n).sum f - (range m).sum f :=
id      └─┘   └─┘     └───┘  └─┘     └───┘  └─┘  
src     └─┘     └─┘      └───┘   └─┘      └───┘   └─┘
typ     └─┘   └─┘     └───┘  └─┘     └───┘  └─┘  
doc     └─┘               └───┘             └───┘
373  sum_Ico_eq_add_neg f h
id   └────────────────┘  
src  └────────────────┘
typ  └────────────────┘  
374  
375  @[to_additive]
doc    └─────────┘
376  lemma prod_Ico_eq_prod_range (f : ℕ → β) (m n : ℕ) :
id                                                 
src                                                 
typ                                                
377    (Ico m n).prod f = (range (n - m)).prod (λ l, f (m + l)) :=
id      └─┘   └──┘     └───┘      └──┘           
src     └─┘     └──┘      └───┘        └──┘             
typ     └─┘   └──┘     └───┘      └──┘           
doc     └─┘     └──┘       └───┘         └──┘
378  begin
st   └─────
379    by_cases h : m ≤ n,
id                    
src    └───────┘ └─┘ 
typ    └───────┘ └─┘
doc    └───────┘ └─┘  
txt    └───────┘ └─┘  
par    └───────┘ └─┘  
pid             └─┘  
st   ───────────────────┘└─
380    { rw [← Ico.zero_bot, prod_Ico_add, zero_add, nat.sub_add_cancel h] },
id             └──────────┘  └──────────┘  └──────┘  └────────────────┘ 
src      └────┘└──────────┘└┘└──────────┘└┘└──────┘└┘└────────────────┘ └┘
typ      └────┘└──────────┘└┘└──────────┘└┘└──────┘└┘└────────────────┘└┘
doc      └────┘            └┘            └┘        └┘                   └┘
txt      └────┘            └┘            └┘        └┘                   └┘
par      └────┘            └┘            └┘        └┘                   └┘
pid        └──┘            └┘            └┘        └┘                   
st   ───┘└────────────────┘└────────────┘└────────┘└────────────────────┘└┘
381    { replace h : n ≤ m :=  le_of_not_ge h,
id                           └──────────┘ 
src      └──────────┘   └───┘└──────────┘
typ      └──────────┘ └───┘└──────────┘
doc      └──────────┘   └───┘            
txt      └──────────┘   └───┘            
par      └──────────┘   └───┘            
pid             └┘└─┘   └───┘            
st   ───────────────────────────────────────┘└─
382       rw [Ico.eq_empty_of_le h, nat.sub_eq_zero_of_le h, range_zero, prod_empty, prod_empty] }
id            └────────────────┘   └───────────────────┘   └────────┘  └────────┘  └────────┘
src       └──┘└────────────────┘ └┘└───────────────────┘ └┘└────────┘└┘└────────┘└┘└────────┘└┘
typ       └──┘└────────────────┘└┘└───────────────────┘└┘└────────┘└┘└────────┘└┘└────────┘└┘
doc       └──┘                   └┘                      └┘          └┘          └┘          └┘
txt       └──┘                   └┘                      └┘          └┘          └┘          └┘
par       └──┘                   └┘                      └┘          └┘          └┘          └┘
pid         └┘                   └┘                      └┘          └┘          └┘          
st   ────────────────────────────┘└───────────────────────┘└──────────┘└──────────┘└──────────┘└─
383  end
st   ──┘
384  
385  @[to_additive]
doc    └─────────┘
386  lemma prod_range_zero (f : ℕ → β) :
id                                 
src                             
typ                                
387   (range 0).prod f = 1 :=
id     └───┘   └──┘   
src    └───┘   └──┘    
typ    └───┘   └──┘   
doc    └───┘   └──┘
388  by rw [range_zero, prod_empty]
id          └────────┘  └────────┘
src     └──┘└────────┘└┘└────────┘└─
typ     └──┘└────────┘└┘└────────┘└─
doc     └──┘          └┘          └─
txt     └──┘          └┘          └─
par     └──┘          └┘          └─
pid       └┘          └┘          
st     └─────────────┘└──────────┘
389  
src  
typ  
doc  
txt  
par  
pid  
st   
390  lemma prod_range_one (f : ℕ → β) :
id                                
src                            
typ                               
391    (range 1).prod f = f 0 :=
id      └───┘   └──┘    
src     └───┘   └──┘    
typ     └───┘   └──┘    
doc     └───┘   └──┘
392  by { rw [range_one], apply @prod_singleton ℕ β 0 f }
id            └───────┘          └────────────┘      
src       └──┘└───────┘  └────┘ └────────────┘  └─┘ 
typ       └──┘└───────┘  └────┘ └────────────┘ └─┘
doc       └──┘           └────┘                 └─┘ 
txt       └──┘           └────┘                 └─┘ 
par       └──┘           └────┘                 └─┘ 
pid         └┘                                 └─┘ 
st     └──────────────┘└───────────────────────────────┘└┘
393  
394  lemma sum_range_one {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) :
id                                    └─────────────┘           
src                                   └─────────────┘         
typ                                   └─────────────┘           
395    (range 1).sum f = f 0 :=
id      └───┘   └─┘    
src     └───┘   └─┘    
typ     └───┘   └─┘    
doc     └───┘
396  by { rw [range_one], apply @sum_singleton ℕ δ 0 f }
id            └───────┘          └───────────┘      
src       └──┘└───────┘  └────┘ └───────────┘  └─┘ 
typ       └──┘└───────┘  └────┘ └───────────┘ └─┘
doc       └──┘           └────┘                └─┘ 
txt       └──┘           └────┘                └─┘ 
par       └──┘           └────┘                └─┘ 
pid         └┘                                └─┘ 
st     └──────────────┘└──────────────────────────────┘└┘
397  
398  attribute [to_additive finset.sum_range_one] prod_range_one
id                                                └────────────┘
src                                               └────────────┘
typ                                               └────────────┘
doc             └─────────┘
399  
400  @[simp] lemma prod_const (b : β) : s.prod (λ a, b) = b ^ s.card :=
id                                     └───┘           └───┘
src                                      └───┘               └───┘
typ                                    └───┘           └───┘
doc    └──┘                              └───┘                 └───┘
401  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
402  finset.induction_on s rfl (λ a s has ih,
id   └─────────────────┘  └─┘
src  └─────────────────┘ └─┘  └───────────┘
typ  └─────────────────┘└─┘  └───────────┘
doc  └─────────────────┘      └───────────┘
txt                           └───────────┘
par                           └───────────┘
pid                           └───────────┘
st   ─────────────────────────────────────────
403  by rw [prod_insert has, card_insert_of_not_mem has, pow_succ, ih])
id          └─────────┘ └─┘  └────────────────────┘ └─┘  └──────┘  └┘
src    └──┘└─────────┘   └┘└────────────────────┘   └┘└──────┘└┘  └─
typ    └──┘└─────────┘└─┘└┘└────────────────────┘└─┘└┘└──────┘└┘└┘└─
doc    └──┘              └┘                         └┘        └┘  └─
txt    └──┘              └┘                         └┘        └┘  └─
par    └──┘              └┘                         └┘        └┘  └─
pid    └───┘              └┘                         └┘        └┘  └┘
st   ─┘└──────────────────┘└──────────────────────────┘└────────┘└──┘└─
404  
src  
typ  
doc  
txt  
par  
pid  
st   
405  lemma prod_pow (s : finset α) (n : ℕ) (f : α → β) :
id                       └────┘                  
src                      └────┘         
typ                      └────┘                  
doc                      └────┘
406    s.prod (λ x, f x ^ n) = s.prod f ^ n :=
id     └───┘            └───┘   
src     └───┘                 └───┘   
typ    └───┘            └───┘   
doc     └───┘                   └───┘
407  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
408  finset.induction_on s (by simp) (by simp [_root_.mul_pow] {contextual := tt})
id   └─────────────────┘                      └────────────┘                 └┘
src  └─────────────────┘    └──┘└┘   └────┘└────────────┘└┘ └────────────┘└┘└─
typ  └─────────────────┘   └──┘└┘   └────┘└────────────┘└┘ └────────────┘└┘└─
doc  └─────────────────┘    └──┘└┘   └────┘              └┘ └────────────┘  └─
txt                         └──┘└┘   └────┘              └┘ └────────────┘  └─
par                         └──┘└┘   └────┘              └┘ └────────────┘  └─
pid                         └─────┘   └─────┘              └┘ └────────────┘  └┘
st   ────────────────────────┘└───┘└───┘└───────────────────────────────────────┘└─
409  
src  
typ  
doc  
txt  
par  
pid  
st   
410  lemma prod_nat_pow (s : finset α) (n : ℕ) (f : α → ℕ) :
id                           └────┘                  
src                          └────┘                    
typ                          └────┘                  
doc                          └────┘
411    s.prod (λ x, f x ^ n) = s.prod f ^ n :=
id     └───┘            └───┘   
src     └───┘                 └───┘   
typ    └───┘            └───┘   
doc     └───┘                   └───┘
412  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
413  finset.induction_on s (by simp) (by simp [nat.mul_pow] {contextual := tt})
id   └─────────────────┘                      └─────────┘                 └┘
src  └─────────────────┘    └──┘└┘   └────┘└─────────┘└┘ └────────────┘└┘└─
typ  └─────────────────┘   └──┘└┘   └────┘└─────────┘└┘ └────────────┘└┘└─
doc  └─────────────────┘    └──┘└┘   └────┘           └┘ └────────────┘  └─
txt                         └──┘└┘   └────┘           └┘ └────────────┘  └─
par                         └──┘└┘   └────┘           └┘ └────────────┘  └─
pid                         └─────┘   └─────┘           └┘ └────────────┘  └┘
st   ────────────────────────┘└───┘└───┘└────────────────────────────────────┘└─
414  
src  
typ  
doc  
txt  
par  
pid  
st   
415  @[to_additive]
doc    └─────────┘
416  lemma prod_involution {s : finset α} {f : α → β} :
id                              └────┘           
src                             └────┘
typ                             └────┘           
doc                             └────┘
417    ∀ (g : Π a ∈ s, α)
id                   
typ                  
418    (h₁ : ∀ a ha, f a * f (g a ha) = 1)
id              └┘         └┘  
src                                  
typ             └┘         └┘  
419    (h₂ : ∀ a ha, f a ≠ 1 → g a ha ≠ a)
id              └┘           └┘  
src                                  
typ             └┘           └┘  
420    (h₃ : ∀ a ha, g a ha ∈ s)
id              └┘    └┘  
src                         
typ             └┘    └┘  
421    (h₄ : ∀ a ha, g (g a ha) (h₃ a ha) = a),
id              └┘      └┘   └┘  └┘   
src                                       
typ             └┘      └┘   └┘  └┘   
422    s.prod f = 1 :=
id     └───┘  
src     └───┘   
typ    └───┘  
doc     └───┘
423  by haveI := classical.dec_eq α;
id               └──────────────┘ 
src     └───────┘└──────────────┘
typ     └───────┘└──────────────┘
doc     └───────┘                
txt     └───────┘                
par     └───────┘                
pid          └─┘                
st     └─────────────────────────────
424  haveI := classical.dec_eq β; exact
id            └──────────────┘ 
src  └───────┘└──────────────┘   └────┘
typ  └───────┘└──────────────┘  └────┘
doc  └───────┘                   └────┘
txt  └───────┘                   └────┘
par  └───────┘                   └────┘
pid       └─┘                        
st   ───────────────────────────────────
425  finset.strong_induction_on s
id   └────────────────────────┘ 
src  └────────────────────────┘ 
typ  └────────────────────────┘
doc                             
txt                             
par                             
pid                             
st   ─────────────────────────────
426    (λ s ih g h₁ h₂ h₃ h₄,
src  ─┘  └────────────────────
typ  ─┘  └────────────────────
doc  ─┘  └────────────────────
txt  ─┘  └────────────────────
par  ─┘  └────────────────────
pid  ─┘  └────────────────────
st   ─────────────────────────
427      s.eq_empty_or_nonempty.elim (λ hs, hs.symm ▸ rfl)
id        └───────────────────┘└───┘          └───┘  └─┘
src  ───┘ └───────────────────┘└───┘  └───┘  └───┘└─┘└─
typ  ───┘ └───────────────────┘└───┘  └───┘  └───┘└─┘└─
doc  ───┘                             └───┘           └─
txt  ───┘                             └───┘           └─
par  ───┘                             └───┘           └─
pid  ───┘                             └───┘           └─
st   ──────────────────────────────────────────────────────
428        (λ ⟨x, hx⟩,
id               └┘
src  ─────┘  └┘ └┘  └──
typ  ─────┘  └┘└┘└┘└──
doc  ─────┘  └┘ └┘  └──
txt  ─────┘  └┘ └┘  └──
par  ─────┘  └┘ └┘  └──
pid  ─────┘  └┘ └┘  └──
st   ──────────────────
429        have hmem : ∀ y ∈ (s.erase x).erase (g x hx), y ∈ s,
id                            └────┘                        
src  ─────┘    └──────┘ └───┘  └────┘ └──────┘         └─
typ  ─────┘    └──────┘ └───┘ └────┘ └──────┘        └─
doc  ─────┘    └──────┘ └───┘  └────┘ └──────┘         └─
txt  ─────┘    └──────┘ └───┘         └──────┘         └─
par  ─────┘    └──────┘ └───┘         └──────┘         └─
pid  ─────┘    └──────┘ └───┘         └──────┘         └─
st   ───────────────────────────────────────────────────────────
430          from λ y hy, (mem_of_mem_erase (mem_of_mem_erase hy)),
id                                           └──────────────┘
src  ────────────┘ └─────┘                  └──────────────┘  └───
typ  ────────────┘ └─────┘                  └──────────────┘  └───
doc  ────────────┘ └─────┘                                    └───
txt  ────────────┘ └─────┘                                    └───
par  ────────────┘ └─────┘                                    └───
pid  ────────────┘ └─────┘                                    └───
st   ───────────────────────────────────────────────────────────────
431        have g_inj : ∀ {x hx y hy}, g x hx = g y hy → x = y,
id                                           
src  ─────┘    └───────┘ └──────────┘             └─
typ  ─────┘    └───────┘ └──────────┘            └─
doc  ─────┘    └───────┘ └──────────┘              └─
txt  ─────┘    └───────┘ └──────────┘              └─
par  ─────┘    └───────┘ └──────────┘              └─
pid  ─────┘    └───────┘ └──────────┘              └─
st   ───────────────────────────────────────────────────────────
432          from λ x hx y hy h, by rw [← h₄ x hx, ← h₄ y hy]; simp [h],
id                                        └┘  └┘    └┘  └┘         
src  ────────────┘ └────────────┘  └────┘     └──┘     └┘└────┘ └─
typ  ────────────┘ └────────────┘  └────┘└┘└┘└──┘└┘└┘└┘└────┘└─
doc  ────────────┘ └────────────┘  └────┘     └──┘     └┘└────┘ └─
txt  ────────────┘ └────────────┘  └────┘     └──┘     └┘└────┘ └─
par  ────────────┘ └────────────┘  └────┘     └──┘     └┘└────┘ └─
pid  ────────────┘ └────────────┘  └─────┘     └──┘     └───────┘ └──
st   ─────────────────────────────┘└────────────┘└─────────┘└────────┘└─
433        have ih': (erase (erase s x) (g x hx)).prod f = (1 : β) :=
id                           └───┘                             
src  ─────┘    └────┘       └───┘  └┘     └──────┘   └──┘ └────
typ  ─────┘    └────┘       └───┘  └┘    └──────┘   └──┘└────
doc  ─────┘    └────┘       └───┘  └┘     └──────┘   └──┘ └────
txt  ─────┘    └────┘              └┘     └──────┘   └──┘ └────
par  ─────┘    └────┘              └┘     └──────┘   └──┘ └────
pid  ─────┘    └────┘              └┘     └──────┘   └──┘ └────
st   ─────────────────────────────────────────────────────────────────
434          ih ((s.erase x).erase (g x hx))
id                 └────┘
src  ───────┘     └────┘ └──────┘     └──
typ  ───────┘     └────┘ └──────┘     └──
doc  ───────┘     └────┘ └──────┘     └──
txt  ───────┘            └──────┘     └──
par  ───────┘            └──────┘     └──
pid  ───────┘            └──────┘     └──
st   ────────────────────────────────────────
435            ⟨subset.trans (erase_subset _ _) (erase_subset _ _),
id              └──────────┘                     └──────────┘
src  ─────────┘ └──────────┘             └────┘ └──────────┘└──────
typ  ─────────┘ └──────────┘             └────┘ └──────────┘└──────
doc  ─────────┘                          └────┘             └──────
txt  ─────────┘                          └────┘             └──────
par  ─────────┘                          └────┘             └──────
pid  ─────────┘                          └────┘             └──────
st   ───────────────────────────────────────────────────────────────
436              λ h, not_mem_erase (g x hx) (s.erase x) (h (h₃ x hx))⟩
id                    └───────────┘            └────┘
src  ───────────┘ └──┘└───────────┘     └┘  └────┘ └┘        └───
typ  ───────────┘ └──┘└───────────┘     └┘  └────┘ └┘        └───
doc  ───────────┘ └──┘                  └┘  └────┘ └┘        └───
txt  ───────────┘ └──┘                  └┘         └┘        └───
par  ───────────┘ └──┘                  └┘         └┘        └───
pid  ───────────┘ └──┘                  └┘         └┘        └───
st   ───────────────────────────────────────────────────────────────────
437            (λ y hy, g y (hmem y hy))
src  ─────────┘  └─────┘          └──
typ  ─────────┘  └─────┘          └──
doc  ─────────┘  └─────┘          └──
txt  ─────────┘  └─────┘          └──
par  ─────────┘  └─────┘          └──
pid  ─────────┘  └─────┘          └──
st   ────────────────────────────────────
438            (λ y hy, h₁ y (hmem y hy))
src  ─────────┘  └─────┘           └──
typ  ─────────┘  └─────┘           └──
doc  ─────────┘  └─────┘           └──
txt  ─────────┘  └─────┘           └──
par  ─────────┘  └─────┘           └──
pid  ─────────┘  └─────┘           └──
st   ─────────────────────────────────────
439            (λ y hy, h₂ y (hmem y hy))
src  ─────────┘  └─────┘           └──
typ  ─────────┘  └─────┘           └──
doc  ─────────┘  └─────┘           └──
txt  ─────────┘  └─────┘           └──
par  ─────────┘  └─────┘           └──
pid  ─────────┘  └─────┘           └──
st   ─────────────────────────────────────
440            (λ y hy, mem_erase.2 ⟨λ (h : g y _ = g x hx), by simpa [g_inj h] using hy,
id                                                                    └───┘         └┘
src  ─────────┘  └─────┘         └─┘  └────┘  └─┘     └─┘  └─────┘      └──────┘  └─
typ  ─────────┘  └─────┘         └─┘  └────┘  └─┘    └─┘  └─────┘└───┘└──────┘└┘└─
doc  ─────────┘  └─────┘         └─┘  └────┘  └─┘     └─┘  └─────┘      └──────┘  └─
txt  ─────────┘  └─────┘         └─┘  └────┘  └─┘     └─┘  └─────┘      └──────┘  └─
par  ─────────┘  └─────┘         └─┘  └────┘  └─┘     └─┘  └─────┘      └──────┘  └─
pid  ─────────┘  └─────┘         └─┘  └────┘  └─┘     └─┘  └──────┘      └──────┘  └─
st   ─────────────────────────────────────────────────────────┘└───────────────────────┘└─
441              mem_erase.2 ⟨λ (h : g y _ = x),
id               └───────┘                 
src  ───────────┘└───────┘└─┘  └────┘  └─┘  └──
typ  ───────────┘└───────┘└─┘  └────┘  └─┘ └──
doc  ───────────┘         └─┘  └────┘  └─┘  └──
txt  ───────────┘         └─┘  └────┘  └─┘  └──
par  ───────────┘         └─┘  └────┘  └─┘  └──
pid  ───────────┘         └─┘  └────┘  └─┘  └──
st   ────────────────────────────────────────────
442                have y = g x hx, from h₄ y (hmem y hy) ▸ by simp [h],
id                                                                   
src  ─────────────┘    └─┘     └─────┘           └┘   └────┘ └─
typ  ─────────────┘    └─┘     └─────┘           └┘   └────┘└─
doc  ─────────────┘    └─┘     └─────┘           └┘   └────┘ └─
txt  ─────────────┘    └─┘     └─────┘           └┘   └────┘ └─
par  ─────────────┘    └─┘     └─────┘           └┘   └────┘ └─
pid  ─────────────┘    └─┘     └─────┘           └┘   └─────┘ └──
st   ────────────────────────────────────────────────────────┘└───────┘└─
443                by simpa [this] using hy, h₃ y (hmem y hy)⟩⟩)
id                           └──┘        └┘
src  ─────────────┘  └─────┘    └──────┘  └┘           └────
typ  ─────────────┘  └─────┘└──┘└──────┘└┘└┘           └────
doc  ─────────────┘  └─────┘    └──────┘  └┘           └────
txt  ─────────────┘  └─────┘    └──────┘  └┘           └────
par  ─────────────┘  └─────┘    └──────┘  └┘           └────
pid  ─────────────┘  └──────┘    └──────┘  └┘           └────
st   ───────────────┘└────────────────────┘└─────────────────────
444            (λ y hy, h₄ y (hmem y hy)),
src  ─────────┘  └─────┘           └───
typ  ─────────┘  └─────┘           └───
doc  ─────────┘  └─────┘           └───
txt  ─────────┘  └─────┘           └───
par  ─────────┘  └─────┘           └───
pid  ─────────┘  └─────┘           └───
st   ──────────────────────────────────────
445        if hx1 : f x = 1
id         └┘          
src  ─────┘└┘└─────┘   └──
typ  ─────┘└┘└─────┘ └──
doc  ─────┘  └─────┘   └──
txt  ─────┘  └─────┘   └──
par  ─────┘  └─────┘   └──
pid  ─────┘  └─────┘   └──
st   ───────────────────────
446        then ih' ▸ eq.symm (prod_subset hmem
id                    └─────┘  └─────────┘
src  ──────────┘    └─────┘ └─────────┘    
typ  ──────────┘    └─────┘ └─────────┘    
doc  ──────────┘                           
txt  ──────────┘                           
par  ──────────┘                           
pid  ──────────┘                           
st   ───────────────────────────────────────────
447          (λ y hy hy₁,
src  ───────┘  └──────────
typ  ───────┘  └──────────
doc  ───────┘  └──────────
txt  ───────┘  └──────────
par  ───────┘  └──────────
pid  ───────┘  └──────────
st   ─────────────────────
448            have y = x ∨ y = g x hx, by simp [hy] at hy₁; tauto,
id                                             └┘
src  ─────────┘    └─┘        └───┘└────┘  └──────┘└┘└───┘└─
typ  ─────────┘    └─┘       └───┘└────┘└┘└──────┘└┘└───┘└─
doc  ─────────┘    └─┘         └───┘└────┘  └──────┘└┘└───┘└─
txt  ─────────┘    └─┘         └───┘└────┘  └──────┘└┘└───┘└─
par  ─────────┘    └─┘         └───┘└────┘  └──────┘└┘└───┘└─
pid  ─────────┘    └─┘         └─────────┘  └────────────────
st   ────────────────────────────────────┘└──────────────────────┘└─
449            this.elim (λ h, h.symm ▸ hx1)
id                 └───┘
src  ─────────┘    └───┘  └──┘          └─
typ  ─────────┘    └───┘  └──┘          └─
doc  ─────────┘           └──┘          └─
txt  ─────────┘           └──┘          └─
par  ─────────┘           └──┘          └─
pid  ─────────┘           └──┘          └─
st   ────────────────────────────────────────
450              (λ h, h₁ x hx ▸ h ▸ hx1.symm ▸ (one_mul _).symm)))
id                     └┘               └───┘    └─────┘
src  ───────────┘  └──┘           └───┘  └─────┘└───────────
typ  ───────────┘  └──┘└┘         └───┘  └─────┘└───────────
doc  ───────────┘  └──┘                         └───────────
txt  ───────────┘  └──┘                         └───────────
par  ───────────┘  └──┘                         └───────────
pid  ───────────┘  └──┘                         └───────────
st   ───────────────────────────────────────────────────────────────
451        else by rw [← insert_erase hx, prod_insert (not_mem_erase _ _),
id                       └──────────┘ └┘  └─────────┘  └───────────┘
src  ──────────┘  └────┘└──────────┘  └┘└─────────┘ └───────────┘└──────
typ  ──────────┘  └────┘└──────────┘└┘└┘└─────────┘ └───────────┘└──────
doc  ──────────┘  └────┘              └┘                         └──────
txt  ──────────┘  └────┘              └┘                         └──────
par  ──────────┘  └────┘              └┘                         └──────
pid  ──────────┘  └─────┘              └┘                         └──────
st   ────────────┘└────────────────────┘└───────────────────────────────┘└─
452          ← insert_erase (mem_erase.2 ⟨h₂ x hx hx1, h₃ x hx⟩),
id             └──────────┘  └───────┘    └┘      └─┘  └┘  └┘
src  ─────────┘└──────────┘ └───────┘└─┘         └┘     └───
typ  ─────────┘└──────────┘ └───────┘└─┘ └┘   └─┘└┘└┘└┘└───
doc  ─────────┘                      └─┘         └┘     └───
txt  ─────────┘                      └─┘         └┘     └───
par  ─────────┘                      └─┘         └┘     └───
pid  ─────────┘                      └─┘         └┘     └───
st   ──────────────────────────────────────────────────────────┘└─
453          prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx]))
id           └─────────┘  └───────────┘       └─┘  └─────┘  └┘  └┘
src  ───────┘└─────────┘ └───────────┘└─────┘   └┘└─────┘└┘     └──
typ  ───────┘└─────────┘ └───────────┘└─────┘└─┘└┘└─────┘└┘└┘└┘└──
doc  ───────┘                         └─────┘   └┘       └┘     └──
txt  ───────┘                         └─────┘   └┘       └┘     └──
par  ───────┘                         └─────┘   └┘       └┘     └──
pid  ───────┘                         └─────┘   └┘       └┘     └─┘
st   ──────────────────────────────────────┘└───┘└───────┘└───────┘└──
454  
src  
typ  
doc  
txt  
par  
pid  
st   
455  @[to_additive]
doc    └─────────┘
456  lemma prod_eq_one {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : s.prod f = 1 :=
id                                    └────┘                    └───┘  
src                                     └────┘                          └───┘   
typ                                   └────┘                    └───┘  
doc                                     └────┘                           └───┘
457  calc s.prod f = s.prod (λx, 1) : finset.prod_congr rfl h
id        └───┘    └───┘          └───────────────┘ └─┘ 
src        └───┘      └───┘           └───────────────┘ └─┘
typ       └───┘    └───┘          └───────────────┘ └─┘ 
doc        └───┘      └───┘
458    ... = 1 : finset.prod_const_one
id               └───────────────────┘
src              └───────────────────┘
typ              └───────────────────┘
459  
460  /-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
461  of `s`, and over all subsets of `s` to which one adds `x`. -/
462  @[to_additive]
doc    └─────────┘
463  lemma prod_powerset_insert [decidable_eq α] {s : finset α} {x : α} (h : x ∉ s) (f : finset α → β) :
id                               └──────────┘        └────┘                        └────┘    
src                              └──────────┘         └────┘                            └────┘
typ                              └──────────┘        └────┘                        └────┘    
doc                                                   └────┘                             └────┘
464    (insert x s).powerset.prod f = s.powerset.prod f * s.powerset.prod (λt, f (insert x t)) :=
id      └────┘   └──────┘ └──┘    └───────┘└───┘   └───────┘└───┘       └────┘  
src     └────┘     └──────┘ └──┘      └───────┘└───┘     └───────┘└───┘         └────┘
typ     └────┘   └──────┘ └──┘    └───────┘└───┘   └───────┘└───┘       └────┘  
doc                └──────┘ └──┘       └───────┘└───┘      └───────┘└───┘
465  begin
st   └─────
466    rw [powerset_insert, finset.prod_union, finset.prod_image],
id         └─────────────┘  └───────────────┘  └───────────────┘
src    └──┘└─────────────┘└┘└───────────────┘└┘└───────────────┘
typ    └──┘└─────────────┘└┘└───────────────┘└┘└───────────────┘
doc    └──┘               └┘                 └┘                 
txt    └──┘               └┘                 └┘                 
par    └──┘               └┘                 └┘                 
pid      └┘               └┘                 └┘                 
st   ────────────────────┘└─────────────────┘└─────────────────┘└──
467    { assume t₁ h₁ t₂ h₂ heq,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid      └────────────────────┘
st   ───┘└────────────────────┘└─
468      rw [← finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₁ h),
id             └─────────────────┘  └────────────────────────────────┘ └┘ 
src      └────┘└─────────────────┘ └────────────────────────────────┘   └──
typ      └────┘└─────────────────┘ └────────────────────────────────┘└┘└──
doc      └────┘                                                         └──
txt      └────┘                                                         └──
par      └────┘                                                         └──
pid        └──┘                                                         └──
st   ──────────────────────────────────────────────────────────────────────┘└─
469          ← finset.erase_insert (not_mem_of_mem_powerset_of_not_mem h₂ h), heq] },
id             └─────────────────┘  └────────────────────────────────┘ └┘    └─┘
src  ─────────┘└─────────────────┘ └────────────────────────────────┘   └─┘└─┘└┘
typ  ─────────┘└─────────────────┘ └────────────────────────────────┘└┘└─┘└─┘└┘
doc  ─────────┘                                                         └─┘   └┘
txt  ─────────┘                                                         └─┘   └┘
par  ─────────┘                                                         └─┘   └┘
pid  ─────────┘                                                         └─┘   
st   ──────────────────────────────────────────────────────────────────────┘└───┘└┘
470    { rw finset.disjoint_iff_ne,
id          └────────────────────┘
src      └─┘└────────────────────┘
typ      └─┘└────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────────────────┘└─
471      assume t₁ h₁ t₂ h₂,
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid      └────────────────┘
st   ─────────────────────┘└─
472      rcases finset.mem_image.1 h₂ with ⟨t₃, h₃, H₃₂⟩,
id              └──────────────┘   └┘
src      └─────┘└──────────────┘└─┘  └─────────────────┘
typ      └─────┘└──────────────┘└─┘└┘└─────────────────┘
doc      └─────┘                └─┘  └─────────────────┘
txt      └─────┘                └─┘  └─────────────────┘
par      └─────┘                └─┘  └─────────────────┘
pid                            └─┘  └─────────────────┘
st   ──────────────────────────────────────────────────┘└─
473      rw ← H₃₂,
id            └─┘
src      └───┘
typ      └───┘└─┘
doc      └───┘
txt      └───┘
par      └───┘
pid        └─┘
st   ───────────┘└─
474      exact ne_insert_of_not_mem _ _ (not_mem_of_mem_powerset_of_not_mem h₁ h) }
id             └──────────────────┘      └────────────────────────────────┘ └┘ 
src      └────┘└──────────────────┘└───┘ └────────────────────────────────┘   └┘
typ      └────┘└──────────────────┘└───┘ └────────────────────────────────┘└┘└┘
doc      └────┘                    └───┘                                      └┘
txt      └────┘                    └───┘                                      └┘
par      └────┘                    └───┘                                      └┘
pid                               └───┘                                      
st   ────────────────────────────────────────────────────────────────────────────┘└─
475  end
st   ──┘
476  
477  @[to_additive]
doc    └─────────┘
478  lemma prod_piecewise [decidable_eq α] (s t : finset α) (f g : α → β) :
id                         └──────────┘          └────┘             
src                        └──────────┘           └────┘
typ                        └──────────┘          └────┘             
doc                                               └────┘
479    s.prod (t.piecewise f g) = (s ∩ t).prod f * (s \ t).prod g :=
id     └───┘  └────────┘         └──┘        └──┘  
src     └───┘   └────────┘             └──┘           └──┘
typ    └───┘  └────────┘         └──┘        └──┘  
doc     └───┘   └────────┘               └──┘             └──┘
480  by { rw [piecewise, prod_ite _ _ (λ x, x), filter_mem_eq_inter, ← sdiff_eq_filter], assumption }
id            └───────┘  └──────┘               └─────────────────┘    └─────────────┘
src       └──┘└───────┘└┘└──────┘└───┘  └──┘ └─┘└─────────────────┘└──┘└─────────────┘  └─────────┘
typ       └──┘└───────┘└┘└──────┘└───┘  └──┘ └─┘└─────────────────┘└──┘└─────────────┘  └─────────┘
doc       └──┘└───────┘└┘        └───┘  └──┘ └─┘                   └──┘                 └─────────┘
txt       └──┘         └┘        └───┘  └──┘ └─┘                   └──┘                 └─────────┘
par       └──┘         └┘        └───┘  └──┘ └─┘                   └──┘                 └─────────┘
pid         └┘         └┘        └───┘  └──┘ └─┘                   └──┘                           
st     └──────────────┘└─────────────────────┘└───────────────────┘└─────────────────┘└────────────┘└┘
481  
482  /-- If we can partition a product into subsets that cancel out, then the whole product cancels. -/
483  @[to_additive]
doc    └─────────┘
484  lemma prod_cancels_of_partition_cancels (R : setoid α) [decidable_rel R.r]
id                                                └────┘    └───────────┘ └┘
src                                               └────┘     └───────────┘  └┘
typ                                               └────┘    └───────────┘ └┘
485    (h : ∀ x ∈ s, (s.filter (λy, y ≈ x)).prod f = 1) : s.prod f = 1 :=
id                  └─────┘         └──┘         └───┘  
src                    └─────┘            └──┘           └───┘   
typ                 └─────┘         └──┘         └───┘  
doc                    └─────┘             └──┘            └───┘
486  begin
st   └─────
487    suffices : (s.image quotient.mk).prod (λ xbar, (s.filter (λ y, ⟦y⟧ = xbar)).prod f) = s.prod f,
id                 └─────┘ └─────────┘                 └──────┘                             └────┘ 
src    └─────────┘ └─────┘└─────────┘└─────┘  └─────┘ └──────┘  └──┘       └──────┘ └┘ └────┘
typ    └─────────┘ └─────┘└─────────┘└─────┘  └─────┘ └──────┘  └──┘       └──────┘ └┘ └────┘
doc    └─────────┘ └─────┘           └─────┘  └─────┘ └──────┘  └──┘        └──────┘ └┘ └────┘
txt    └─────────┘                   └─────┘  └─────┘           └──┘        └──────┘ └┘       
par    └─────────┘                   └─────┘  └─────┘           └──┘        └──────┘ └┘       
pid    └───────┘└┘                   └─────┘  └─────┘           └──┘        └──────┘ └┘       
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
488    { rw [←this, ←finset.prod_eq_one],
id            └──┘   └────────────────┘
src      └───┘    └─┘└────────────────┘
typ      └───┘└──┘└─┘└────────────────┘
doc      └───┘    └─┘                  
txt      └───┘    └─┘                  
par      └───┘    └─┘                  
pid        └─┘    └─┘                  
st   ───┘└───────┘└───────────────────┘└─
489      intros xbar xbar_in_s,
src      └───────────────────┘
typ      └───────────────────┘
doc      └───────────────────┘
txt      └───────────────────┘
par      └───────────────────┘
pid            └─────────────┘
st   ────────────────────────┘└─
490      rcases (mem_image).mp xbar_in_s with ⟨x, x_in_s, xbar_eq_x⟩,
id               └───────┘     └───────┘
src      └─────┘ └───────┘└───┘         └──────────────────────────┘
typ      └─────┘ └───────┘└───┘└───────┘└──────────────────────────┘
doc      └─────┘          └───┘         └──────────────────────────┘
txt      └─────┘          └───┘         └──────────────────────────┘
par      └─────┘          └───┘         └──────────────────────────┘
pid                      └───┘         └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
491      rw [←xbar_eq_x, filter_congr (λ y _, @quotient.eq _ R y x)],
id            └───────┘  └──────────┘          └─────────┘      
src      └───┘         └┘└──────────┘  └────┘ └─────────┘└─┘   └┘
typ      └───┘└───────┘└┘└──────────┘  └────┘ └─────────┘└─┘ └┘
doc      └───┘         └┘              └────┘            └─┘   └┘
txt      └───┘         └┘              └────┘            └─┘   └┘
par      └───┘         └┘              └────┘            └─┘   └┘
pid        └─┘         └┘              └────┘            └─┘   └┘
st   ─────────────────┘└──────────────────────────────────────────┘└──
492      apply h x x_in_s },
id               └────┘
src      └────┘        
typ      └────┘└────┘
doc      └────┘        
txt      └────┘        
par      └────┘        
pid                   
st   ────────────────────┘└┘
493    apply finset.prod_image' f,
id           └────────────────┘ 
src    └────┘└────────────────┘
typ    └────┘└────────────────┘
doc    └────┘                  
txt    └────┘                  
par    └────┘                  
pid                           
st   ───────────────────────────┘└─
494    intros,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
495    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
496  end
st   └─┘
497  
498  @[to_additive]
doc    └─────────┘
499  lemma prod_update_of_not_mem [decidable_eq α] {s : finset α} {i : α}
id                                 └──────────┘        └────┘        
src                                └──────────┘         └────┘
typ                                └──────────┘        └────┘        
doc                                                     └────┘
500    (h : i ∉ s) (f : α → β) (b : β) : s.prod (function.update f i b) = s.prod f :=
id                                 └───┘  └─────────────┘      └───┘ 
src                                      └───┘  └─────────────┘          └───┘
typ                                └───┘  └─────────────┘      └───┘ 
doc                                       └───┘  └─────────────┘           └───┘
501  begin
st   └─────
502    apply prod_congr rfl (λj hj, _),
id           └────────┘ └─┘
src    └────┘└────────┘└─┘  └──────┘
typ    └────┘└────────┘└─┘  └──────┘
doc    └────┘               └──────┘
txt    └────┘               └──────┘
par    └────┘               └──────┘
pid                        └──────┘
st   ────────────────────────────────┘└─
503    have : j ≠ i, by { assume eq, rw eq at hj, exact h hj },
id                                   └┘               └┘
src    └─────┘         └───────┘  └─┘└┘└────┘  └────┘   
typ    └─────┘       └───────┘  └─┘└┘└────┘  └────┘└┘
doc    └─────┘          └───────┘  └─┘  └────┘  └────┘   
txt    └─────┘          └───────┘  └─┘  └────┘  └────┘   
par    └─────┘          └───────┘  └─┘  └────┘  └────┘   
pid    └───┘└┘          └───────┘      └────┘          
st   ─────────────┘     └────────┘└───────────┘└───────────┘└┘
504    simp [this]
id           └──┘
src    └────┘    └┘
typ    └────┘└──┘└┘
doc    └────┘    └┘
txt    └────┘    └┘
par    └────┘    └┘
pid            
st   ─────────────┘
505  end
st   └─┘
506  
507  lemma prod_update_of_mem [decidable_eq α] {s : finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) :
id                             └──────────┘        └────┘                                  
src                            └──────────┘         └────┘                   
typ                            └──────────┘        └────┘                                  
doc                                                 └────┘
508    s.prod (function.update f i b) = b * (s \ (singleton i)).prod f :=
id     └───┘  └─────────────┘            └───────┘   └──┘  
src     └───┘  └─────────────┘                 └───────┘    └──┘
typ    └───┘  └─────────────┘            └───────┘   └──┘  
doc     └───┘  └─────────────┘                    └───────┘    └──┘
509  by { rw [update_eq_piecewise, prod_piecewise], simp [h] }
id            └─────────────────┘  └────────────┘         
src       └──┘└─────────────────┘└┘└────────────┘  └────┘ └┘
typ       └──┘└─────────────────┘└┘└────────────┘  └────┘└┘
doc       └──┘                   └┘                └────┘ └┘
txt       └──┘                   └┘                └────┘ └┘
par       └──┘                   └┘                └────┘ └┘
pid         └┘                   └┘                     
st     └────────────────────────┘└──────────────┘└──────────┘└┘
510  
511  end comm_monoid
512  
513  lemma sum_update_of_mem [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α}
id                            └─────────────┘    └──────────┘        └────┘        
src                           └─────────────┘     └──────────┘         └────┘
typ                           └─────────────┘    └──────────┘        └────┘        
doc                                                                    └────┘
514    (h : i ∈ s) (f : α → β) (b : β) :
id                             
src           
typ                            
515    s.sum (function.update f i b) = b + (s \ (singleton i)).sum f :=
id     └──┘  └─────────────┘            └───────┘   └─┘  
src     └──┘  └─────────────┘                 └───────┘    └─┘
typ    └──┘  └─────────────┘            └───────┘   └─┘  
doc           └─────────────┘                    └───────┘
516  by { rw [update_eq_piecewise, sum_piecewise], simp [h] }
id            └─────────────────┘  └───────────┘         
src       └──┘└─────────────────┘└┘└───────────┘  └────┘ └┘
typ       └──┘└─────────────────┘└┘└───────────┘  └────┘└┘
doc       └──┘                   └┘               └────┘ └┘
txt       └──┘                   └┘               └────┘ └┘
par       └──┘                   └┘               └────┘ └┘
pid         └┘                   └┘                    
st     └────────────────────────┘└─────────────┘└──────────┘└┘
517  attribute [to_additive] prod_update_of_mem
id                           └────────────────┘
src                          └────────────────┘
typ                          └────────────────┘
doc             └─────────┘
518  
519  lemma sum_smul' [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
id                    └─────────────┘        └────┘                  
src                   └─────────────┘         └────┘         
typ                   └─────────────┘        └────┘                  
doc                                           └────┘
520    s.sum (λ x, add_monoid.smul n (f x)) = add_monoid.smul n (s.sum f) :=
id     └──┘      └─────────────┘        └─────────────┘   └──┘ 
src     └──┘       └─────────────┘           └─────────────┘     └──┘
typ    └──┘      └─────────────┘        └─────────────┘   └──┘ 
521  @prod_pow _ (multiplicative β) _ _ _ _
id    └──────┘    └────────────┘ 
src   └──────┘    └────────────┘
typ   └──────┘    └────────────┘ 
522  attribute [to_additive sum_smul'] prod_pow
id                                     └──────┘
src                                    └──────┘
typ                                    └──────┘
doc             └─────────┘
523  
524  @[simp] lemma sum_const [add_comm_monoid β] (b : β) :
id                            └─────────────┘        
src                           └─────────────┘
typ                           └─────────────┘        
doc    └──┘
525    s.sum (λ a, b) = add_monoid.smul s.card b :=
id     └──┘         └─────────────┘ └───┘ 
src     └──┘           └─────────────┘  └───┘
typ    └──┘         └─────────────┘ └───┘ 
doc                                      └───┘
526  @prod_const _ (multiplicative β) _ _ _
id    └────────┘    └────────────┘ 
src   └────────┘    └────────────┘
typ   └────────┘    └────────────┘ 
527  attribute [to_additive] prod_const
id                           └────────┘
src                          └────────┘
typ                          └────────┘
doc             └─────────┘
528  
529  lemma sum_range_succ' [add_comm_monoid β] (f : ℕ → β) :
id                          └─────────────┘           
src                         └─────────────┘         
typ                         └─────────────┘           
530    ∀ n : ℕ, (range (nat.succ n)).sum f = (range n).sum (f ∘ nat.succ) + f 0 :=
id              └───┘  └──────┘   └─┘     └───┘  └─┘     └──────┘   
src             └───┘  └──────┘    └─┘      └───┘   └─┘      └──────┘  
typ             └───┘  └──────┘   └─┘     └───┘  └─┘     └──────┘   
doc              └───┘                        └───┘
531  @prod_range_succ' (multiplicative β) _ _
id    └──────────────┘  └────────────┘ 
src   └──────────────┘  └────────────┘
typ   └──────────────┘  └────────────┘ 
532  attribute [to_additive] prod_range_succ'
id                           └──────────────┘
src                          └──────────────┘
typ                          └──────────────┘
doc             └─────────┘
533  
534  lemma sum_nat_cast [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) :
id                       └─────────────┘    └─────┘        └────┘           
src                      └─────────────┘     └─────┘         └────┘             
typ                      └─────────────┘    └─────┘        └────┘           
doc                                                          └────┘
535    ↑(s.sum f) = s.sum (λa, f a : α → β) :=
id      └──┘    └──┘            
src      └──┘      └──┘
typ     └──┘    └──┘            
536  (s.sum_hom _).symm
id    └──────┘   └──┘
src    └──────┘   └──┘
typ   └──────┘   └──┘
537  
538  lemma prod_nat_cast [comm_semiring β] (s : finset α) (f : α → ℕ) :
id                        └───────────┘        └────┘           
src                       └───────────┘         └────┘             
typ                       └───────────┘        └────┘           
doc                                             └────┘
539    ↑(s.prod f) = s.prod (λa, f a : α → β) :=
id      └───┘    └───┘            
src      └───┘      └───┘
typ     └───┘    └───┘            
doc       └───┘       └───┘
540  (s.prod_hom _).symm
id    └───────┘   └──┘
src    └───────┘   └──┘
typ   └───────┘   └──┘
541  
542  protected lemma sum_nat_coe_enat [decidable_eq α] (s : finset α) (f : α → ℕ) :
id                                     └──────────┘        └────┘           
src                                    └──────────┘         └────┘             
typ                                    └──────────┘        └────┘           
doc                                                         └────┘
543    s.sum (λ x, (f x : enat)) = (s.sum f : ℕ) :=
id     └──┘           └──┘     └──┘    
src     └──┘              └──┘      └──┘     
typ    └──┘           └──┘     └──┘    
544  begin
st   └─────
545    induction s using finset.induction with a s has ih h,
id               
src    └────────┘ └───────────────────────────────────────┘
typ    └────────┘└───────────────────────────────────────┘
doc    └────────┘ └───────────────────────────────────────┘
txt    └────────┘ └───────────────────────────────────────┘
par    └────────┘ └───────────────────────────────────────┘
pid              └─────────────────────┘└────────────────┘
st   ─────────────────────────────────────────────────────┘└─
546    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
547    { simp [has, ih] }
id             └─┘  └┘
src      └────┘   └┘  └┘
typ      └────┘└─┘└┘└┘└┘
doc      └────┘   └┘  └┘
txt      └────┘   └┘  └┘
par      └────┘   └┘  └┘
pid             └┘  
st   ──────────────────┘└─
548  end
st   ──┘
549  
550  theorem dvd_sum [comm_semiring α] {a : α} {s : finset β} {f : β → α}
id                    └───────────┘               └────┘           
src                   └───────────┘                 └────┘
typ                   └───────────┘               └────┘           
doc                                                 └────┘
551    (h : ∀ x ∈ s, a ∣ f x) : a ∣ s.sum f :=
id                          └──┘ 
src                                └──┘
typ                         └──┘ 
552  multiset.dvd_sum (λ y hy, by rcases multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx)
id   └──────────────┘     └┘            └──────────────┘   └┘                            └┘
src  └──────────────┘             └─────┘└──────────────┘└─┘  └────────────────┘  └────┘  
typ  └──────────────┘     └┘     └─────┘└──────────────┘└─┘└┘└────────────────┘  └────┘└┘
doc                               └─────┘                └─┘  └────────────────┘  └────┘  
txt                               └─────┘                └─┘  └────────────────┘  └────┘  
par                               └─────┘                └─┘  └────────────────┘  └────┘  
pid                                                     └─┘  └────────────────┘         
st                               └───────────────────────────────────────────────────────────┘
553  
554  lemma le_sum_of_subadditive [add_comm_monoid α] [ordered_comm_monoid β]
id                                └─────────────┘    └─────────────────┘ 
src                               └─────────────┘     └─────────────────┘
typ                               └─────────────┘    └─────────────────┘ 
doc                                                   └─────────────────┘
555    (f : α → β) (h_zero : f 0 = 0) (h_add : ∀x y, f (x + y) ≤ f x + f y) (s : finset γ) (g : γ → α) :
id                                                               └────┘           
src                                                                          └────┘
typ                                                              └────┘           
doc                                                                              └────┘
556    f (s.sum g) ≤ s.sum (λc, f (g c)) :=
id       └──┘    └──┘        
src        └──┘      └──┘
typ      └──┘    └──┘        
557  begin
st   └─────
558    refine le_trans (multiset.le_sum_of_subadditive f h_zero h_add _) _,
id            └──────┘  └────────────────────────────┘  └────┘ └───┘
src    └─────┘└──────┘ └────────────────────────────┘            └───┘
typ    └─────┘└──────┘ └────────────────────────────┘└────┘└───┘└───┘
doc    └─────┘                                                   └───┘
txt    └─────┘                                                   └───┘
par    └─────┘                                                   └───┘
pid                                                             └───┘
st   ────────────────────────────────────────────────────────────────────┘└─
559    rw [multiset.map_map],
id         └──────────────┘
src    └──┘└──────────────┘
typ    └──┘└──────────────┘
doc    └──┘                
txt    └──┘                
par    └──┘                
pid      └┘                
st   ─────────────────────┘└──
560    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
561  end
st   └─┘
562  
563  lemma abs_sum_le_sum_abs [discrete_linear_ordered_field α] {f : β → α} {s : finset β} :
id                             └───────────────────────────┘                  └────┘ 
src                            └───────────────────────────┘                     └────┘
typ                            └───────────────────────────┘                  └────┘ 
doc                                                                              └────┘
564    abs (s.sum f) ≤ s.sum (λa, abs (f a)) :=
id     └─┘  └──┘    └──┘     └─┘   
src    └─┘   └──┘      └──┘      └─┘
typ    └─┘  └──┘    └──┘     └─┘   
565  le_sum_of_subadditive _ abs_zero abs_add s f
id   └───────────────────┘   └──────┘ └─────┘  
src  └───────────────────┘   └──────┘ └─────┘
typ  └───────────────────┘   └──────┘ └─────┘  
566  
567  section comm_group
568  variables [comm_group β]
id              └────────┘
src             └────────┘
typ             └────────┘
569  
570  @[simp, to_additive]
doc    └──┘  └─────────┘
571  lemma prod_inv_distrib : s.prod (λx, (f x)⁻¹) = (s.prod f)⁻¹ :=
id                            └───┘        └┘    └───┘  └┘
src                            └───┘           └┘     └───┘   └┘
typ                           └───┘        └┘    └───┘  └┘
doc                            └───┘                   └───┘
572  s.prod_hom has_inv.inv
id   └───────┘ └─────────┘
src   └───────┘ └─────────┘
typ  └───────┘ └─────────┘
573  
574  end comm_group
575  
576  @[simp] theorem card_sigma {σ : α → Type*} (s : finset α) (t : Π a, finset (σ a)) :
id                                                  └────┘            └────┘   
src                                                  └────┘              └────┘
typ                                                 └────┘            └────┘   
doc    └──┘                                          └────┘              └────┘
577    card (s.sigma t) = s.sum (λ a, card (t a)) :=
id     └──┘  └────┘    └──┘      └──┘   
src    └──┘   └────┘      └──┘       └──┘
typ    └──┘  └────┘    └──┘      └──┘   
doc    └──┘   └────┘                  └──┘
578  multiset.card_sigma _ _
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
579  
580  lemma card_bind [decidable_eq β] {s : finset α} {t : α → finset β}
id                    └──────────┘        └────┘           └────┘ 
src                   └──────────┘         └────┘             └────┘
typ                   └──────────┘        └────┘           └────┘ 
doc                                        └────┘             └────┘
581    (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → disjoint (t x) (t y)) :
id                             └──────┘       
src                                  └──────┘
typ                            └──────┘       
doc                                   └──────┘
582    (s.bind t).card = s.sum (λ u, card (t u)) :=
id      └───┘  └──┘   └──┘      └──┘   
src      └───┘   └──┘    └──┘       └──┘
typ     └───┘  └──┘   └──┘      └──┘   
doc      └───┘   └──┘                └──┘
583  calc (s.bind t).card = (s.bind t).sum (λ _, 1) : by simp
id         └───┘  └──┘     └───┘  └─┘     
src         └───┘   └──┘      └───┘   └─┘                └───┘
typ        └───┘  └──┘     └───┘  └─┘               └───┘
doc         └───┘   └──┘      └───┘                      └───┘
txt                                                      └───┘
par                                                      └───┘
pid                                                          
st                                                      └────┘
584  ... = s.sum (λ a, (t a).sum (λ _, 1)) : finset.sum_bind h
id         └──┘         └─┘             └─────────────┘ 
src         └──┘            └─┘              └─────────────┘
typ        └──┘         └─┘             └─────────────┘ 
585  ... = s.sum (λ u, card (t u)) : by simp
id         └──┘      └──┘   
src         └──┘       └──┘             └────
typ        └──┘      └──┘           └────
doc                    └──┘             └────
txt                                     └────
par                                     └────
pid                                         
st                                     └─────
586  
src  
typ  
doc  
txt  
par  
pid  
st   
587  lemma card_bind_le [decidable_eq β] {s : finset α} {t : α → finset β} :
id                       └──────────┘        └────┘           └────┘ 
src                      └──────────┘         └────┘             └────┘
typ                      └──────────┘        └────┘           └────┘ 
doc                                           └────┘             └────┘
588    (s.bind t).card ≤ s.sum (λ a, (t a).card) :=
id      └───┘  └──┘   └──┘         └──┘
src      └───┘   └──┘    └──┘            └──┘
typ     └───┘  └──┘   └──┘         └──┘
doc      └───┘   └──┘                     └──┘
589  by haveI := classical.dec_eq α; exact
id               └──────────────┘ 
src     └───────┘└──────────────┘   └────┘
typ     └───────┘└──────────────┘  └────┘
doc     └───────┘                   └────┘
txt     └───────┘                   └────┘
par     └───────┘                   └────┘
pid          └─┘                        
st     └───────────────────────────────────
590  finset.induction_on s (by simp)
id   └─────────────────┘ 
src  └─────────────────┘    └──┘└─
typ  └─────────────────┘   └──┘└─
doc  └─────────────────┘    └──┘└─
txt                         └──┘└─
par                         └──┘└─
pid                         └──────
st   ────────────────────────┘└───┘└─
591    (λ a s has ih,
src  ─┘  └────────────
typ  ─┘  └────────────
doc  ─┘  └────────────
txt  ─┘  └────────────
par  ─┘  └────────────
pid  ─┘  └────────────
st   ─────────────────
592      calc ((insert a s).bind t).card ≤ (t a).card + (s.bind t).card :
id                                                       └───┘
src  ───┘              └─────┘ └─────┘    └─────┘  └───┘ └────────
typ  ───┘              └─────┘ └─────┘    └─────┘  └───┘ └────────
doc  ───┘              └─────┘ └─────┘    └─────┘   └───┘ └────────
txt  ───┘              └─────┘ └─────┘    └─────┘         └────────
par  ───┘              └─────┘ └─────┘    └─────┘         └────────
pid  ───┘              └─────┘ └─────┘    └─────┘         └────────
st   ─────────────────────────────────────────────────────────────────────
593      by rw bind_insert; exact finset.card_union_le _ _
id             └─────────┘        └──────────────────┘
src  ───┘  └─┘└─────────┘└──────┘└──────────────────┘└────
typ  ───┘  └─┘└─────────┘└──────┘└──────────────────┘└────
doc  ───┘  └─┘           └──────┘                    └────
txt  ───┘  └─┘           └──────┘                    └────
par  ───┘  └─┘           └──────┘                    └────
pid  ───┘  └──┘           └──────┘                    └────
st   ─────┘└───────────────────────────────────────────────
594      ... ≤ (insert a s).sum (λ a, card (t a)) :
id              └────┘                └──┘  
src  ───────┘  └────┘  └────┘  └──┘└──┘   └────
typ  ───────┘  └────┘  └────┘  └──┘└──┘  └────
doc  ───────┘          └────┘  └──┘└──┘   └────
txt  ───────┘          └────┘  └──┘       └────
par  ───────┘          └────┘  └──┘       └────
pid  ───────┘          └────┘  └──┘       └────
st   ───┘└──────────────────────────────────────────
595      by rw sum_insert has; exact add_le_add_left ih _)
id             └────────┘ └─┘        └─────────────┘ └┘
src  ───┘  └─┘└────────┘   └──────┘└─────────────┘  └───
typ  ───┘  └─┘└────────┘└─┘└──────┘└─────────────┘└┘└───
doc  ───┘  └─┘             └──────┘                 └───
txt  ───┘  └─┘             └──────┘                 └───
par  ───┘  └─┘             └──────┘                 └───
pid  ───┘  └──┘             └──────┘                 └─┘
st   ─────┘└────────────────────────────────────────────┘└─
596  
src  
typ  
doc  
txt  
par  
pid  
st   
597  theorem card_eq_sum_card_image [decidable_eq β] (f : α → β) (s : finset α) :
id                                   └──────────┘                  └────┘ 
src                                  └──────────┘                     └────┘
typ                                  └──────────┘                  └────┘ 
doc                                                                   └────┘
598    s.card = (s.image f).sum (λ a, (s.filter (λ x, f x = a)).card) :=
id     └───┘   └────┘  └─┘        └─────┘           └──┘
src     └───┘    └────┘   └─┘          └─────┘               └──┘
typ    └───┘   └────┘  └─┘        └─────┘           └──┘
doc     └───┘     └────┘                └─────┘                └──┘
599  by letI := classical.dec_eq α; exact
id              └──────────────┘ 
src     └──────┘└──────────────┘   └────┘
typ     └──────┘└──────────────┘  └────┘
doc     └──────┘                   └────┘
txt     └──────┘                   └────┘
par     └──────┘                   └────┘
pid         └─┘                        
st     └──────────────────────────────────
600  calc s.card = ((s.image f).bind (λ a, s.filter (λ x, f x = a))).card :
id        └────┘                                              
src      └────┘           └─────┘  └──┘          └──┘   └──────────
typ      └────┘           └─────┘  └──┘          └──┘   └──────────
doc      └────┘           └─────┘  └──┘          └──┘    └──────────
txt                       └─────┘  └──┘          └──┘    └──────────
par                       └─────┘  └──┘          └──┘    └──────────
pid                       └─────┘  └──┘          └──┘    └──────────
st   ───────────────────────────────────────────────────────────────────────
601    congr_arg _ (finset.ext.2 $ λ x,
id     └───────┘    └────────┘
src  ─┘└───────┘└─┘ └────────┘└─┘  └───
typ  ─┘└───────┘└─┘ └────────┘└─┘  └───
doc  ─┘         └─┘           └─┘  └───
txt  ─┘         └─┘           └─┘  └───
par  ─┘         └─┘           └─┘  └───
pid  ─┘         └─┘           └─┘  └───
st   ───────────────────────────────────
602      ⟨λ hs, mem_bind.2 ⟨f x, mem_image_of_mem _ hs,
id                              └──────────────┘
src  ───┘  └───┘        └─┘   └┘└──────────────┘└─┘  └─
typ  ───┘  └───┘        └─┘  └┘└──────────────┘└─┘  └─
doc  ───┘  └───┘        └─┘   └┘                └─┘  └─
txt  ───┘  └───┘        └─┘   └┘                └─┘  └─
par  ───┘  └───┘        └─┘   └┘                └─┘  └─
pid  ───┘  └───┘        └─┘   └┘                └─┘  └─
st   ───────────────────────────────────────────────────
603        mem_filter.2 ⟨hs, rfl⟩⟩,
id         └────────┘        └─┘
src  ─────┘└────────┘└─┘   └┘└─┘└───
typ  ─────┘└────────┘└─┘   └┘└─┘└───
doc  ─────┘          └─┘   └┘   └───
txt  ─────┘          └─┘   └┘   └───
par  ─────┘          └─┘   └┘   └───
pid  ─────┘          └─┘   └┘   └───
st   ───────────────────────────────
604      λ h, let ⟨a, ha₁, ha₂⟩ := mem_bind.1 h in by convert filter_subset s ha₂⟩)
id                                 └──────┘                   └───────────┘  └─┘
src  ───┘ └──┘     └┘   └┘   └───┘└──────┘└─┘ └──┘  └──────┘└───────────┘    └──
typ  ───┘ └──┘     └┘   └┘   └───┘└──────┘└─┘ └──┘  └──────┘└───────────┘└─┘└──
doc  ───┘ └──┘     └┘   └┘   └───┘        └─┘ └──┘  └──────┘                 └──
txt  ───┘ └──┘     └┘   └┘   └───┘        └─┘ └──┘  └──────┘                 └──
par  ───┘ └──┘     └┘   └┘   └───┘        └─┘ └──┘  └──────┘                 └──
pid  ───┘ └──┘     └┘   └┘   └───┘        └─┘ └──┘  └───────┘                 └──
st   ───────────────────────────────────────────────┘└──────────────────────────┘└──
605  ... = (s.image f).sum (λ a, (s.filter (λ x, f x = a)).card) :
id          └─────┘               └──────┘
src  ───┘  └─────┘ └────┘  └──┘ └──────┘  └──┘    └──────────
typ  ───┘  └─────┘ └────┘  └──┘ └──────┘  └──┘    └──────────
doc  ───┘  └─────┘ └────┘  └──┘ └──────┘  └──┘    └──────────
txt  ───┘          └────┘  └──┘           └──┘    └──────────
par  ───┘          └────┘  └──┘           └──┘    └──────────
pid  ───┘          └────┘  └──┘           └──┘    └──────────
st   ──────────────────────────────────────────────────────────────
606    card_bind (by simp [disjoint_left, finset.ext] {contextual := tt})
id     └───────┘           └───────────┘  └────────┘                 └┘
src  ─┘└───────┘   └────┘└───────────┘└┘└────────┘└┘ └────────────┘└┘└─
typ  ─┘└───────┘   └────┘└───────────┘└┘└────────┘└┘ └────────────┘└┘└─
doc  ─┘            └────┘             └┘          └┘ └────────────┘  └─
txt  ─┘            └────┘             └┘          └┘ └────────────┘  └─
par  ─┘            └────┘             └┘          └┘ └────────────┘  └─
pid  ─┘            └─────┘             └┘          └┘ └────────────┘  └┘
st   ──────────────┘└──────────────────────────────────────────────────┘└─
607  
src  
typ  
doc  
txt  
par  
pid  
st   
608  lemma gsmul_sum [add_comm_group β] {f : α → β} {s : finset α} (z : ℤ) :
id                    └────────────┘                  └────┘        
src                   └────────────┘                     └────┘         
typ                   └────────────┘                  └────┘        
doc                                                      └────┘
609    gsmul z (s.sum f) = s.sum (λa, gsmul z (f a)) :=
id     └───┘   └──┘    └──┘     └───┘    
src    └───┘     └──┘      └──┘      └───┘
typ    └───┘   └──┘    └──┘     └───┘    
610  (s.sum_hom (gsmul z)).symm
id    └──────┘  └───┘   └──┘
src    └──────┘  └───┘    └──┘
typ   └──────┘  └───┘   └──┘
611  
612  end finset
613  
614  namespace finset
615  variables {s s₁ s₂ : finset α} {f g : α → β} {b : β} {a : α}
id                        └────┘
src                       └────┘
typ                       └────┘
doc                       └────┘
616  
617  @[simp] lemma sum_sub_distrib [add_comm_group β] : s.sum (λx, f x - g x) = s.sum f - s.sum g :=
id                                  └────────────┘     └──┘            └──┘   └──┘ 
src                                 └────────────┘       └──┘                  └──┘     └──┘
typ                                 └────────────┘     └──┘            └──┘   └──┘ 
doc    └──┘
618  sum_add_distrib.trans $ congr_arg _ sum_neg_distrib
id   └─────────────┘└────┘   └───────┘   └─────────────┘
src  └─────────────┘└────┘   └───────┘   └─────────────┘
typ  └─────────────┘└────┘   └───────┘   └─────────────┘
619  
620  section semiring
621  variables [semiring β]
id              └──────┘
src             └──────┘
typ             └──────┘
622  
623  lemma sum_mul : s.sum f * b = s.sum (λx, f x * b) :=
id                   └──┘     └──┘        
src                   └──┘        └──┘          
typ                  └──┘     └──┘        
624  (s.sum_hom (λ x, x * b)).symm
id    └──────┘          └──┘
src    └──────┘             └──┘
typ   └──────┘          └──┘
625  
626  lemma mul_sum : b * s.sum f = s.sum (λx, b * f x) :=
id                     └──┘   └──┘        
src                      └──┘     └──┘        
typ                    └──┘   └──┘        
627  (s.sum_hom _).symm
id    └──────┘   └──┘
src    └──────┘   └──┘
typ   └──────┘   └──┘
628  
629  @[simp] lemma sum_mul_boole [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
id                                └──────────┘        └────┘                  
src                               └──────────┘         └────┘
typ                               └──────────┘        └────┘                  
doc    └──┘                                            └────┘
630    s.sum (λ x, (f x * ite (a = x) 1 0)) = ite (a ∈ s) (f a) 0 :=
id     └──┘          └─┘             └─┘        
src     └──┘             └─┘               └─┘    
typ    └──┘          └─┘             └─┘        
631  begin
st   └─────
632    convert sum_ite_eq s a f,
id             └────────┘   
src    └──────┘└────────┘  
typ    └──────┘└────────┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid                       
st   ─────────────────────────┘└─
633    funext,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
634    split_ifs with h; simp [h],
id                             
src    └──────────────┘  └────┘ 
typ    └──────────────┘  └────┘
doc    └──────────────┘  └────┘ 
txt    └──────────────┘  └────┘ 
par    └──────────────┘  └────┘ 
pid             └────┘       
st   ───────────────────────────┘└─
635  end
st   ──┘
636  @[simp] lemma sum_boole_mul [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
id                                └──────────┘        └────┘                  
src                               └──────────┘         └────┘
typ                               └──────────┘        └────┘                  
doc    └──┘                                            └────┘
637    s.sum (λ x, (ite (a = x) 1 0) * f x) = ite (a ∈ s) (f a) 0 :=
id     └──┘       └─┘                └─┘        
src     └──┘        └─┘                    └─┘    
typ    └──┘       └─┘                └─┘        
638  begin
st   └─────
639    convert sum_ite_eq s a f,
id             └────────┘   
src    └──────┘└────────┘  
typ    └──────┘└────────┘
doc    └──────┘            
txt    └──────┘            
par    └──────┘            
pid                       
st   ─────────────────────────┘└─
640    funext,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
641    split_ifs with h; simp [h],
id                             
src    └──────────────┘  └────┘ 
typ    └──────────────┘  └────┘
doc    └──────────────┘  └────┘ 
txt    └──────────────┘  └────┘ 
par    └──────────────┘  └────┘ 
pid             └────┘       
st   ───────────────────────────┘└─
642  end
st   ──┘
643  
644  end semiring
645  
646  section comm_semiring
647  variables [decidable_eq α] [comm_semiring β]
id              └──────────┘     └───────────┘
src             └──────────┘     └───────────┘
typ             └──────────┘     └───────────┘
648  
649  lemma prod_eq_zero (ha : a ∈ s) (h : f a = 0) : s.prod f = 0 :=
id                                             └───┘  
src                                                 └───┘   
typ                                            └───┘  
doc                                                   └───┘
650  calc s.prod f = (insert a (erase s a)).prod f : by rw insert_erase ha
id        └───┘     └────┘   └───┘    └──┘           └──────────┘ └┘
src        └───┘      └────┘    └───┘      └──┘         └─┘└──────────┘  
typ       └───┘     └────┘   └───┘    └──┘        └─┘└──────────┘└┘
doc        └───┘                └───┘      └──┘         └─┘              
txt                                                     └─┘              
par                                                     └─┘              
pid                                                                     
st                                                     └───────────────────
651    ... = 0 : by rw [prod_insert (not_mem_erase _ _), h, zero_mul]
id                      └─────────┘  └───────────┘         └──────┘
src  ─┘             └──┘└─────────┘ └───────────┘└─────┘ └┘└──────┘└─
typ  ─┘             └──┘└─────────┘ └───────────┘└─────┘└┘└──────┘└─
doc  ─┘             └──┘                         └─────┘ └┘        └─
txt  ─┘             └──┘                         └─────┘ └┘        └─
par  ─┘             └──┘                         └─────┘ └┘        └─
pid  ─┘               └┘                         └─────┘ └┘        
st   ─┘            └──────────────────────────────────┘└─┘└────────┘
652  
src  
typ  
doc  
txt  
par  
pid  
st   
653  lemma prod_sum {δ : α → Type*} [∀a, decidable_eq (δ a)]
id                                     └──────────┘   
src                                      └──────────┘    
typ                                    └──────────┘   
654    {s : finset α} {t : Πa, finset (δ a)} {f : Πa, δ a → β} :
id          └────┘           └────┘                  
src         └────┘             └────┘
typ         └────┘           └────┘                  
doc         └────┘             └────┘
655    s.prod (λa, (t a).sum (λb, f a b)) =
id     └───┘        └─┘           
src     └───┘           └─┘               
typ    └───┘        └─┘           
doc     └───┘
656      (s.pi t).sum (λp, s.attach.prod (λx, f x.1 (p x.1 x.2))) :=
id        └─┘  └─┘      └─────┘└───┘            
src        └─┘   └─┘        └─────┘└───┘                  
typ       └─┘  └─┘      └─────┘└───┘            
doc                         └─────┘└───┘
657  begin
st   └─────
658    induction s using finset.induction with a s ha ih,
id               
src    └────────┘ └────────────────────────────────────┘
typ    └────────┘└────────────────────────────────────┘
doc    └────────┘ └────────────────────────────────────┘
txt    └────────┘ └────────────────────────────────────┘
par    └────────┘ └────────────────────────────────────┘
pid              └─────────────────────┘└─────────────┘
st   ──────────────────────────────────────────────────┘└─
659    { rw [pi_empty, sum_singleton], refl },
id           └──────┘  └───────────┘
src      └──┘└──────┘└┘└───────────┘  └───┘
typ      └──┘└──────┘└┘└───────────┘  └───┘
doc      └──┘        └┘               └───┘
txt      └──┘        └┘               └───┘
par      └──┘        └┘               └───┘
pid        └┘        └┘                   
st   ───┘└──────────┘└─────────────┘└─────┘└┘
660    { have h₁ : ∀x ∈ t a, ∀y ∈ t a, ∀h : x ≠ y,
id                                            
src      └────────┘ └──┘    └──┘    └──┘   
typ      └────────┘ └──┘    └──┘    └──┘   
doc      └────────┘ └──┘    └──┘    └──┘    
txt      └────────┘ └──┘    └──┘    └──┘    
par      └────────┘ └──┘    └──┘    └──┘    
pid      └─────┘└─┘ └──┘    └──┘    └──┘    
st   ──────────────────────────────────────────────
661          disjoint (image (pi.cons s a x) (pi s t)) (image (pi.cons s a y) (pi s t)),
id           └──────┘                                   └───┘  └─────┘        └┘  
src  ───────┘└──────┘                 └┘     └─┘ └───┘ └─────┘   └┘ └┘  └┘
typ  ───────┘└──────┘                 └┘     └─┘ └───┘ └─────┘  └┘ └┘└┘
doc  ───────┘└──────┘                 └┘     └─┘ └───┘           └┘     └┘
txt  ───────┘                         └┘     └─┘                 └┘     └┘
par  ───────┘                         └┘     └─┘                 └┘     └┘
pid  ───────┘                         └┘     └─┘                 └┘     └┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
662      { assume x hx y hy h,
src        └────────────────┘
typ        └────────────────┘
doc        └────────────────┘
txt        └────────────────┘
par        └────────────────┘
pid        └────────────────┘
st   ─────┘└────────────────┘└─
663        simp only [disjoint_iff_ne, mem_image],
id                    └─────────────┘  └───────┘
src        └─────────┘└─────────────┘└┘└───────┘
typ        └─────────┘└─────────────┘└┘└───────┘
doc        └─────────┘               └┘         
txt        └─────────┘               └┘         
par        └─────────┘               └┘         
pid            └──┘└┘               └┘         
st   ───────────────────────────────────────────┘└─
664        rintros _ ⟨p₂, hp, eq₂⟩ _ ⟨p₃, hp₃, eq₃⟩ eq,
src        └─────────────────────────────────────────┘
typ        └─────────────────────────────────────────┘
doc        └─────────────────────────────────────────┘
txt        └─────────────────────────────────────────┘
par        └─────────────────────────────────────────┘
pid               └──────────────────────────────────┘
st   ────────────────────────────────────────────────┘└─
665        have : pi.cons s a x p₂ a (mem_insert_self _ _) = pi.cons s a y p₃ a (mem_insert_self _ _),
id                             └┘                          └─────┘     └┘   └─────────────┘
src        └─────┘                             └────┘└─────┘       └─────────────┘└───┘
typ        └─────┘         └┘                 └────┘└─────┘ └┘ └─────────────┘└───┘
doc        └─────┘                             └────┘                              └───┘
txt        └─────┘                             └────┘                              └───┘
par        └─────┘                             └────┘                              └───┘
pid        └───┘└┘                             └────┘                              └───┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
666        { rw [eq₂, eq₃, eq] },
id               └─┘  └─┘  └┘
src          └──┘   └┘   └┘└┘└┘
typ          └──┘└─┘└┘└─┘└┘└┘└┘
doc          └──┘   └┘   └┘  └┘
txt          └──┘   └┘   └┘  └┘
par          └──┘   └┘   └┘  └┘
pid            └┘   └┘   └┘  
st   ───────┘└─────┘└───┘└──┘└┘
667        rw [pi.cons_same, pi.cons_same] at this,
id             └──────────┘  └──────────┘
src        └──┘└──────────┘└┘└──────────┘└───────┘
typ        └──┘└──────────┘└┘└──────────┘└───────┘
doc        └──┘            └┘            └───────┘
txt        └──┘            └┘            └───────┘
par        └──┘            └┘            └───────┘
pid          └┘            └┘            └──────┘
st   ─────────────────────┘└────────────┘└──────┘└─
668        exact h this },
id                └──┘
src        └────┘     
typ        └────┘└──┘
doc        └────┘     
txt        └────┘     
par        └────┘     
pid                  
st   ──────────────────┘└┘
669      rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_bind h₁],
id           └─────────┘ └┘  └───────┘ └┘  └┘  └─────┘  └──────┘ └┘
src      └──┘└─────────┘  └┘└───────┘  └┘  └┘└─────┘└┘└──────┘  
typ      └──┘└─────────┘└┘└┘└───────┘└┘└┘└┘└┘└─────┘└┘└──────┘└┘
doc      └──┘             └┘           └┘  └┘       └┘          
txt      └──┘             └┘           └┘  └┘       └┘          
par      └──┘             └┘           └┘  └┘       └┘          
pid        └┘             └┘           └┘  └┘       └┘          
st   ─────────────────────┘└────────────┘└──┘└───────┘└───────────┘└──
670      refine sum_congr rfl (λ b _, _),
id              └───────┘ └─┘
src      └─────┘└───────┘└─┘  └──────┘
typ      └─────┘└───────┘└─┘  └──────┘
doc      └─────┘              └──────┘
txt      └─────┘              └──────┘
par      └─────┘              └──────┘
pid                          └──────┘
st   ──────────────────────────────────┘└─
671      have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a b p₁ = pi.cons s a b p₂ → p₁ = p₂, from
id                                 └┘                       └─────┘   
src      └────────┘ └─┘      └─┘└┘                └─────┘             └────
typ      └────────┘ └─┘      └─┘└┘              └─────┘          └────
doc      └────────┘ └─┘      └─┘                                      └────
txt      └────────┘ └─┘      └─┘                                      └────
par      └────────┘ └─┘      └─┘                                      └────
pid      └─────┘└─┘ └─┘      └─┘                                      └────
st   ──────────────────────────────────────────────────────────────────────────────────┘└──────
672        assume p₁ h₁ p₂ h₂ eq, injective_pi_cons ha eq,
id                                └───────────────┘ └┘
src  ─────┘      └───────────────┘└───────────────┘  
typ  ─────┘      └───────────────┘└───────────────┘└┘
doc  ─────┘      └───────────────┘                   
txt  ─────┘      └───────────────┘                   
par  ─────┘      └───────────────┘                   
pid  ─────┘      └───────────────┘                   
st   ───────────────────────────────────────────────────┘└─
673      rw [sum_image h₂, mul_sum],
id           └───────┘ └┘  └─────┘
src      └──┘└───────┘  └┘└─────┘
typ      └──┘└───────┘└┘└┘└─────┘
doc      └──┘           └┘       
txt      └──┘           └┘       
par      └──┘           └┘       
pid        └┘           └┘       
st   ───────────────────┘└───────┘└──
674      refine sum_congr rfl (λ g _, _),
id              └───────┘ └─┘
src      └─────┘└───────┘└─┘  └──────┘
typ      └─────┘└───────┘└─┘  └──────┘
doc      └─────┘              └──────┘
txt      └─────┘              └──────┘
par      └─────┘              └──────┘
pid                          └──────┘
st   ──────────────────────────────────┘└─
675      rw [attach_insert, prod_insert, prod_image],
id           └───────────┘  └─────────┘  └────────┘
src      └──┘└───────────┘└┘└─────────┘└┘└────────┘
typ      └──┘└───────────┘└┘└─────────┘└┘└────────┘
doc      └──┘             └┘           └┘          
txt      └──┘             └┘           └┘          
par      └──┘             └┘           └┘          
pid        └┘             └┘           └┘          
st   ────────────────────┘└───────────┘└──────────┘└──
676      { simp only [pi.cons_same],
id                    └──────────┘
src        └─────────┘└──────────┘
typ        └─────────┘└──────────┘
doc        └─────────┘            
txt        └─────────┘            
par        └─────────┘            
pid            └──┘└┘            
st   ─────┘└──────────────────────┘└─
677        congr', ext ⟨v, hv⟩, congr',
src        └────┘  └─────────┘  └────┘
typ        └────┘  └─────────┘  └────┘
doc        └────┘  └─────────┘  └────┘
txt        └────┘  └─────────┘  └────┘
par        └────┘  └─────────┘  └────┘
pid                   └──────┘
st   ───────────┘└───────────┘└──────┘└─
678        exact (pi.cons_ne (by rintro rfl; exact ha hv)).symm },
id                └────────┘                       └┘ └┘
src        └────┘ └────────┘   └────────┘└──────┘    └──────┘
typ        └────┘ └────────┘   └────────┘└──────┘└┘└┘└──────┘
doc        └────┘              └────────┘└──────┘    └──────┘
txt        └────┘              └────────┘└──────┘    └──────┘
par        └────┘              └────────┘└──────┘    └──────┘
pid                           └─────────────────┘    └────┘└┘
st   ──────────────────────────┘└──────────────────────┘└──────┘└┘
679      { exact λ _ _ _ _, subtype.eq ∘ subtype.mk.inj },
id                          └────────┘  └────────────┘
src        └────┘ └────────┘└────────┘└────────────┘
typ        └────┘ └────────┘└────────┘└────────────┘
doc        └────┘ └────────┘                         
txt        └────┘ └────────┘                         
par        └────┘ └────────┘                         
pid              └────────┘                         
st   ─────┘└───────────────────────────────────────────┘└┘
680      { simp only [mem_image], rintro ⟨⟨_, hm⟩, _, rfl⟩, exact ha hm } }
id                    └───────┘                                   └┘ └┘
src        └─────────┘└───────┘  └──────────────────────┘  └────┘    
typ        └─────────┘└───────┘  └──────────────────────┘  └────┘└┘└┘
doc        └─────────┘           └──────────────────────┘  └────┘    
txt        └─────────┘           └──────────────────────┘  └────┘    
par        └─────────┘           └──────────────────────┘  └────┘    
pid            └──┘└┘                 └────────────────┘           
st   ──────────────────────────┘└────────────────────────┘└────────────┘└───
681  end
st   ──┘
682  
683  end comm_semiring
684  
685  section integral_domain /- add integral_semi_domain to support nat and ennreal -/
686  variables [decidable_eq α] [integral_domain β]
id              └──────────┘     └─────────────┘
src             └──────────┘     └─────────────┘
typ             └──────────┘     └─────────────┘
687  
688  lemma prod_eq_zero_iff : s.prod f = 0 ↔ (∃a∈s, f a = 0) :=
id                            └───┘           
src                            └───┘                
typ                           └───┘           
doc                            └───┘
689  finset.induction_on s ⟨not.elim one_ne_zero, λ ⟨_, H, _⟩, H.elim⟩ $ λ a s ha ih,
id   └─────────────────┘   └──────┘ └─────────┘              └───┘        └┘ └┘
src  └─────────────────┘    └──────┘ └─────────┘                └───┘
typ  └─────────────────┘   └──────┘ └─────────┘              └───┘        └┘ └┘
doc  └─────────────────┘
690  by rw [prod_insert ha, mul_eq_zero_iff_eq_zero_or_eq_zero,
id          └─────────┘ └┘  └────────────────────────────────┘
src     └──┘└─────────┘  └┘└────────────────────────────────┘└─
typ     └──┘└─────────┘└┘└┘└────────────────────────────────┘└─
doc     └──┘             └┘                                  └─
txt     └──┘             └┘                                  └─
par     └──┘             └┘                                  └─
pid       └┘             └┘                                  └─
st     └─────────────────┘└──────────────────────────────────┘└─
691    bex_def, exists_mem_insert, ih, ← bex_def]
id     └─────┘  └───────────────┘  └┘    └─────┘
src  ─┘└─────┘└┘└───────────────┘└┘  └──┘└─────┘└─
typ  ─┘└─────┘└┘└───────────────┘└┘└┘└──┘└─────┘└─
doc  ─┘       └┘                 └┘  └──┘       └─
txt  ─┘       └┘                 └┘  └──┘       └─
par  ─┘       └┘                 └┘  └──┘       └─
pid  ─┘       └┘                 └┘  └──┘       
st   ────────┘└─────────────────┘└──┘└─────────┘
692  
src  
typ  
doc  
txt  
par  
pid  
st   
693  end integral_domain
694  
695  section ordered_comm_monoid
696  variables [decidable_eq α] [ordered_comm_monoid β]
id              └──────────┘     └─────────────────┘
src             └──────────┘     └─────────────────┘
typ             └──────────┘     └─────────────────┘
doc                              └─────────────────┘
697  
698  lemma sum_le_sum : (∀x∈s, f x ≤ g x) → s.sum f ≤ s.sum g :=
id                                   └──┘   └──┘ 
src                                         └──┘     └──┘
typ                                  └──┘   └──┘ 
699  finset.induction_on s (λ _, le_refl _) $ assume a s ha ih h,
id   └─────────────────┘       └─────┘               └┘ └┘ 
src  └─────────────────┘         └─────┘
typ  └─────────────────┘       └─────┘               └┘ └┘ 
doc  └─────────────────┘
700    have f a + s.sum f ≤ g a + s.sum g,
id             └──┘      └──┘ 
src               └──┘          └──┘
typ            └──┘      └──┘ 
701      from add_le_add' (h _ (mem_insert_self _ _)) (ih $ assume x hx, h _ $ mem_insert_of_mem hx),
id            └─────────┘      └─────────────┘        └┘           └┘       └───────────────┘ └┘
src           └─────────┘       └─────────────┘                                └───────────────┘
typ           └─────────┘      └─────────────┘        └┘           └┘       └───────────────┘ └┘
702    by simpa only [sum_insert ha]
id                    └────────┘ └┘
src       └──────────┘└────────┘  └─
typ       └──────────┘└────────┘└┘└─
doc       └──────────┘            └─
txt       └──────────┘            └─
par       └──────────┘            └─
pid            └──┘└┘            
st       └───────────────────────────
703  
src  
typ  
doc  
txt  
par  
pid  
st   
704  lemma sum_nonneg (h : ∀x∈s, 0 ≤ f x) : 0 ≤ s.sum f := le_trans (by rw [sum_const_zero]) (sum_le_sum h)
id                                        └──┘     └──────┘         └────────────┘    └────────┘ 
src                                            └──┘      └──────┘     └──┘└────────────┘   └────────┘
typ                                       └──┘     └──────┘     └──┘└────────────┘   └────────┘ 
doc                                                                     └──┘              
txt                                                                     └──┘              
par                                                                     └──┘              
pid                                                                       └┘              
st                                                                     └─────────────────┘
705  
706  lemma sum_nonpos (h : ∀x∈s, f x ≤ 0) : s.sum f ≤ 0 := le_trans (sum_le_sum h) (by rw [sum_const_zero])
id                                     └──┘        └──────┘  └────────┘           └────────────┘
src                                         └──┘         └──────┘  └────────┘        └──┘└────────────┘
typ                                    └──┘        └──────┘  └────────┘       └──┘└────────────┘
doc                                                                                    └──┘              
txt                                                                                    └──┘              
par                                                                                    └──┘              
pid                                                                                      └┘              
st                                                                                    └─────────────────┘
707  
708  lemma sum_le_sum_of_subset_of_nonneg
709    (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → 0 ≤ f x) : s₁.sum f ≤ s₂.sum f :=
id          └┘  └┘          └┘    └┘           └┘└──┘   └┘└──┘ 
src                                                  └──┘      └──┘
typ         └┘  └┘          └┘    └┘           └┘└──┘   └┘└──┘ 
710  calc s₁.sum f ≤ (s₂ \ s₁).sum f + s₁.sum f :
id        └┘└──┘     └┘  └┘ └─┘    └┘└──┘ 
src         └──┘             └─┘       └──┘
typ       └┘└──┘     └┘  └┘ └─┘    └┘└──┘ 
711      le_add_of_nonneg_left' $ sum_nonneg $ by simpa only [mem_sdiff, and_imp]
id       └────────────────────┘   └────────┘                  └───────┘  └─────┘
src      └────────────────────┘   └────────┘      └──────────┘└───────┘└┘└─────┘└─
typ      └────────────────────┘   └────────┘      └──────────┘└───────┘└┘└─────┘└─
doc                                               └──────────┘         └┘       └─
txt                                               └──────────┘         └┘       └─
par                                               └──────────┘         └┘       └─
pid                                                    └──┘└┘         └┘       
st                                               └────────────────────────────────
712    ... = (s₂ \ s₁ ∪ s₁).sum f : (sum_union sdiff_disjoint).symm
id            └┘  └┘  └┘ └─┘      └───────┘ └────────────┘ └──┘
src  ─┘                  └─┘       └───────┘ └────────────┘ └──┘
typ  ─┘       └┘  └┘  └┘ └─┘      └───────┘ └────────────┘ └──┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
713    ... = s₂.sum f : by rw [sdiff_union_of_subset h]
id           └┘└──┘           └───────────────────┘ 
src            └──┘        └──┘└───────────────────┘ └─
typ          └┘└──┘       └──┘└───────────────────┘└─
doc                        └──┘                      └─
txt                        └──┘                      └─
par                        └──┘                      └─
pid                          └┘                      
st                        └──────────────────────────┘
714  
src  
typ  
doc  
txt  
par  
pid  
st   
715  lemma sum_eq_zero_iff_of_nonneg : (∀x∈s, 0 ≤ f x) → (s.sum f = 0 ↔ ∀x∈s, f x = 0) :=
id                                                   └──┘            
src                                                       └──┘                 
typ                                                  └──┘            
716  finset.induction_on s (λ _, ⟨λ _ _, false.elim, λ _, rfl⟩) $ λ a s ha ih H,
id   └─────────────────┘             └────────┘      └─┘         └┘ └┘ 
src  └─────────────────┘                 └────────┘       └─┘
typ  └─────────────────┘             └────────┘      └─┘         └┘ └┘ 
doc  └─────────────────┘
717  have ∀ x ∈ s, 0 ≤ f x, from λ _, H _ ∘ mem_insert_of_mem,
id                                  └───────────────┘
src                                       └───────────────┘
typ                                 └───────────────┘
718  by rw [sum_insert ha,
id          └────────┘ └┘
src     └──┘└────────┘  └─
typ     └──┘└────────┘└┘└─
doc     └──┘            └─
txt     └──┘            └─
par     └──┘            └─
pid       └┘            └─
st     └────────────────┘└─
719    add_eq_zero_iff' (H _ $ mem_insert_self _ _) (sum_nonneg this),
id     └──────────────┘       └─────────────┘       └────────┘ └──┘
src  ─┘└──────────────┘  └─┘ └─────────────┘└────┘ └────────┘    └──
typ  ─┘└──────────────┘ └─┘ └─────────────┘└────┘ └────────┘└──┘└──
doc  ─┘                  └─┘                └────┘               └──
txt  ─┘                  └─┘                └────┘               └──
par  ─┘                  └─┘                └────┘               └──
pid  ─┘                  └─┘                └────┘               └──
st   ───────────────────────────────────────────────────────────────┘└─
720    forall_mem_insert, ih this]
id     └───────────────┘  └┘ └──┘
src  ─┘└───────────────┘└┘      └─
typ  ─┘└───────────────┘└┘└┘└──┘└─
doc  ─┘                 └┘      └─
txt  ─┘                 └┘      └─
par  ─┘                 └┘      └─
pid  ─┘                 └┘      
st   ──────────────────┘└───────┘
721  
src  
typ  
doc  
txt  
par  
pid  
st   
722  lemma sum_eq_zero_iff_of_nonpos : (∀x∈s, f x ≤ 0) → (s.sum f = 0 ↔ ∀x∈s, f x = 0) :=
id                                                   └──┘            
src                                                       └──┘                 
typ                                                  └──┘            
723  @sum_eq_zero_iff_of_nonneg _ (order_dual β) _ _ _ _
id    └───────────────────────┘    └────────┘ 
src   └───────────────────────┘    └────────┘
typ   └───────────────────────┘    └────────┘ 
doc                                └────────┘
724  
725  lemma single_le_sum (hf : ∀x∈s, 0 ≤ f x) {a} (h : a ∈ s) : f a ≤ s.sum f :=
id                                                         └──┘ 
src                                                                 └──┘
typ                                                        └──┘ 
726  have (singleton a).sum f ≤ s.sum f,
id         └───────┘  └─┘    └──┘ 
src        └───────┘   └─┘      └──┘
typ        └───────┘  └─┘    └──┘ 
doc        └───────┘
727    from sum_le_sum_of_subset_of_nonneg
id          └────────────────────────────┘
src         └────────────────────────────┘
typ         └────────────────────────────┘
728    (λ x e, (mem_singleton.1 e).symm ▸ h) (λ x h _, hf x h),
id            └───────────┘   └──┘            └┘  
src             └───────────┘    └──┘  
typ           └───────────┘   └──┘            └┘  
729  by rwa sum_singleton at this
id          └───────────┘
src     └──┘└───────────┘└────────
typ     └──┘└───────────┘└────────
doc     └──┘             └────────
txt     └──┘             └────────
par     └──┘             └────────
pid                     └──────┘
st     └──────────────────────────
730  
src  
typ  
doc  
txt  
par  
pid  
st   
731  end ordered_comm_monoid
732  
733  section canonically_ordered_monoid
734  variables [decidable_eq α] [canonically_ordered_monoid β]
id              └──────────┘     └────────────────────────┘
src             └──────────┘     └────────────────────────┘
typ             └──────────┘     └────────────────────────┘
doc                              └────────────────────────┘
735  
736  lemma sum_le_sum_of_subset (h : s₁ ⊆ s₂) : s₁.sum f ≤ s₂.sum f :=
id                                   └┘  └┘    └┘└──┘   └┘└──┘ 
src                                              └──┘      └──┘
typ                                  └┘  └┘    └┘└──┘   └┘└──┘ 
737  sum_le_sum_of_subset_of_nonneg h $ assume x h₁ h₂, zero_le _
id   └────────────────────────────┘            └┘ └┘  └─────┘
src  └────────────────────────────┘                     └─────┘
typ  └────────────────────────────┘            └┘ └┘  └─────┘
738  
739  lemma sum_le_sum_of_ne_zero [@decidable_rel β (≤)] (h : ∀x∈s₁, f x ≠ 0 → x ∈ s₂) :
id                                 └───────────┘             └┘           └┘
src                                └───────────┘                              
typ                                └───────────┘             └┘           └┘
740    s₁.sum f ≤ s₂.sum f :=
id     └┘└──┘   └┘└──┘ 
src      └──┘      └──┘
typ    └┘└──┘   └┘└──┘ 
741  calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x ≠ 0)).sum f :
id        └┘└──┘     └┘└─────┘           └─┘     └┘└─────┘           └─┘  
src         └──┘        └─────┘              └─┘        └─────┘              └─┘
typ       └┘└──┘     └┘└─────┘           └─┘     └┘└─────┘           └─┘  
doc                     └─────┘                           └─────┘
742      by rw [←sum_union, filter_union_filter_neg_eq];
id               └───────┘  └────────────────────────┘
src         └───┘└───────┘└┘└────────────────────────┘
typ         └───┘└───────┘└┘└────────────────────────┘
doc         └───┘         └┘                          
txt         └───┘         └┘                          
par         └───┘         └┘                          
pid           └─┘         └┘                          
st         └─────────────┘└──────────────────────────┘└─
743         exact disjoint_filter.2 (assume _ _ h n_h, n_h h)
id                └─────────────┘
src         └────┘└─────────────┘└─┘       └──────────┘    └─
typ         └────┘└─────────────┘└─┘       └──────────┘    └─
doc         └────┘               └─┘       └──────────┘    └─
txt         └────┘               └─┘       └──────────┘    └─
par         └────┘               └─┘       └──────────┘    └─
pid                             └─┘       └──────────┘    
st   ─────────────────────────────────────────────────────────
744    ... ≤ s₂.sum f : add_le_of_nonpos_of_le'
id           └┘└──┘    └─────────────────────┘
src  ─┘        └──┘     └─────────────────────┘
typ  ─┘      └┘└──┘    └─────────────────────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
745        (sum_nonpos $ by simp only [mem_filter, and_imp]; exact λ _ _, le_of_eq)
id          └────────┘                 └────────┘  └─────┘                └──────┘
src         └────────┘      └─────────┘└────────┘└┘└─────┘  └────┘ └────┘└──────┘
typ         └────────┘      └─────────┘└────────┘└┘└─────┘  └────┘ └────┘└──────┘
doc                         └─────────┘          └┘         └────┘ └────┘
txt                         └─────────┘          └┘         └────┘ └────┘
par                         └─────────┘          └┘         └────┘ └────┘
pid                             └──┘└┘          └┘               └────┘
st                         └─────────────────────────────────────────────────────┘
746        (sum_le_sum_of_subset $ by simpa only [subset_iff, mem_filter, and_imp])
id          └──────────────────┘                  └────────┘  └────────┘  └─────┘
src         └──────────────────┘      └──────────┘└────────┘└┘└────────┘└┘└─────┘
typ         └──────────────────┘      └──────────┘└────────┘└┘└────────┘└┘└─────┘
doc                                   └──────────┘          └┘          └┘       
txt                                   └──────────┘          └┘          └┘       
par                                   └──────────┘          └┘          └┘       
pid                                        └──┘└┘          └┘          └┘       
st                                   └───────────────────────────────────────────┘
747  
748  end canonically_ordered_monoid
749  
750  section ordered_cancel_comm_monoid
751  
752  variables [ordered_cancel_comm_monoid β]
id              └────────────────────────┘
src             └────────────────────────┘
typ             └────────────────────────┘
753  
754  theorem sum_lt_sum (Hle : ∀ i ∈ s, f i ≤ g i) (Hlt : ∃ i ∈ s, f i < g i) :
id                                                          
src                                                                 
typ                                                         
755    s.sum f < s.sum g :=
id     └──┘   └──┘ 
src     └──┘     └──┘
typ    └──┘   └──┘ 
756  begin
st   └─────
757    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
758    rcases Hlt with ⟨i, hi, hlt⟩,
id            └─┘
src    └─────┘   └────────────────┘
typ    └─────┘└─┘└────────────────┘
doc    └─────┘   └────────────────┘
txt    └─────┘   └────────────────┘
par    └─────┘   └────────────────┘
pid             └────────────────┘
st   ─────────────────────────────┘└─
759    rw [← insert_erase hi, sum_insert (not_mem_erase _ _), sum_insert (not_mem_erase _ _)],
id           └──────────┘ └┘  └────────┘  └───────────┘       └────────┘  └───────────┘
src    └────┘└──────────┘  └┘└────────┘ └───────────┘└─────┘└────────┘ └───────────┘└────┘
typ    └────┘└──────────┘└┘└┘└────────┘ └───────────┘└─────┘└────────┘ └───────────┘└────┘
doc    └────┘              └┘                        └─────┘                        └────┘
txt    └────┘              └┘                        └─────┘                        └────┘
par    └────┘              └┘                        └─────┘                        └────┘
pid      └──┘              └┘                        └─────┘                        └────┘
st   ──────────────────────┘└──────────────────────────────┘└──────────────────────────────┘└──
760    exact add_lt_add_of_lt_of_le hlt (sum_le_sum $ λ j hj, Hle j  $ mem_of_mem_erase hj)
id           └────────────────────┘ └─┘  └────────┘           └─┘      └──────────────┘
src    └────┘└────────────────────┘    └────────┘  └─────┘    └┘ └──────────────┘  └┘
typ    └────┘└────────────────────┘└─┘ └────────┘  └─────┘└─┘ └┘ └──────────────┘  └┘
doc    └────┘                                      └─────┘    └┘                   └┘
txt    └────┘                                      └─────┘    └┘                   └┘
par    └────┘                                      └─────┘    └┘                   └┘
pid                                               └─────┘    └┘                   
st   ──────────────────────────────────────────────────────────────────────────────────────┘
761  end
st   └─┘
762  
763  end ordered_cancel_comm_monoid
764  
765  section decidable_linear_ordered_cancel_comm_monoid
766  
767  variables [decidable_linear_ordered_cancel_comm_monoid β]
id              └─────────────────────────────────────────┘
src             └─────────────────────────────────────────┘
typ             └─────────────────────────────────────────┘
768  
769  theorem exists_le_of_sum_le (hs : s.nonempty) (Hle : s.sum f ≤ s.sum g) :
id                                     └───────┘         └──┘   └──┘ 
src                                     └───────┘          └──┘     └──┘
typ                                    └───────┘         └──┘   └──┘ 
doc                                     └───────┘
770    ∃ i ∈ s, f i ≤ g i :=
id              
src               
typ             
771  begin
st   └─────
772    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
773    contrapose! Hle with Hlt,
src    └──────────────────────┘
typ    └──────────────────────┘
doc    └──────────────────────┘
txt    └──────────────────────┘
par    └──────────────────────┘
pid              └───────────┘
st   ─────────────────────────┘└─
774    rcases hs with ⟨i, hi⟩,
id            └┘
src    └─────┘  └───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
775    exact sum_lt_sum (λ i hi, le_of_lt (Hlt i hi)) ⟨i, hi, Hlt i hi⟩
id           └────────┘          └──────┘                     └─┘  └┘
src    └────┘└────────┘  └─────┘└──────┘       └─┘  └┘  └┘      └┘
typ    └────┘└────────┘  └─────┘└──────┘       └─┘  └┘  └┘└─┘└┘└┘
doc    └────┘            └─────┘               └─┘  └┘  └┘      └┘
txt    └────┘            └─────┘               └─┘  └┘  └┘      └┘
par    └────┘            └─────┘               └─┘  └┘  └┘      └┘
pid                     └─────┘               └─┘  └┘  └┘      
st   ──────────────────────────────────────────────────────────────────┘
776  end
st   └─┘
777  
778  end decidable_linear_ordered_cancel_comm_monoid
779  
780  section linear_ordered_comm_ring
781  variables [decidable_eq α] [linear_ordered_comm_ring β]
id              └──────────┘     └──────────────────────┘
src             └──────────┘     └──────────────────────┘
typ             └──────────┘     └──────────────────────┘
782  
783  /- this is also true for a ordered commutative multiplicative monoid -/
784  lemma prod_nonneg {s : finset α} {f : α → β}
id                          └────┘           
src                         └────┘
typ                         └────┘           
doc                         └────┘
785    (h0 : ∀(x ∈ s), 0 ≤ f x) : 0 ≤ s.prod f :=
id            └┘                 └───┘ 
src                                  └───┘
typ           └┘                 └───┘ 
doc                                    └───┘
786  begin
st   └─────
787    induction s using finset.induction with a s has ih h,
id               
src    └────────┘ └───────────────────────────────────────┘
typ    └────────┘└───────────────────────────────────────┘
doc    └────────┘ └───────────────────────────────────────┘
txt    └────────┘ └───────────────────────────────────────┘
par    └────────┘ └───────────────────────────────────────┘
pid              └─────────────────────┘└────────────────┘
st   ─────────────────────────────────────────────────────┘└─
788    { simp [zero_le_one] },
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ───┘└─────────────────┘└┘
789    { simp [has], apply mul_nonneg, apply h0 a (mem_insert_self a s),
id             └─┘         └────────┘        └┘    └─────────────┘  
src      └────┘     └────┘└────────┘  └────┘    └─────────────┘  
typ      └────┘└─┘  └────┘└────────┘  └────┘└┘  └─────────────┘
doc      └────┘     └────┘            └────┘                     
txt      └────┘     └────┘            └────┘                     
par      └────┘     └────┘            └────┘                     
pid                                                          
st   ─────────────┘└────────────────┘└────────────────────────────────┘└─
790      exact ih (λ x H, h0 x (mem_insert_of_mem H)) }
id             └┘         └┘    └───────────────┘
src      └────┘    └────┘    └───────────────┘ └─┘
typ      └────┘└┘  └────┘└┘  └───────────────┘ └─┘
doc      └────┘    └────┘                      └─┘
txt      └────┘    └────┘                      └─┘
par      └────┘    └────┘                      └─┘
pid               └────┘                      └┘
st   ────────────────────────────────────────────────┘└─
791  end
st   ──┘
792  
793  /- this is also true for a ordered commutative multiplicative monoid -/
794  lemma prod_pos {s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 < f x) : 0 < s.prod f :=
id                       └────┘                    └┘                 └───┘ 
src                      └────┘                                              └───┘
typ                      └────┘                    └┘                 └───┘ 
doc                      └────┘                                                └───┘
795  begin
st   └─────
796    induction s using finset.induction with a s has ih h,
id               
src    └────────┘ └───────────────────────────────────────┘
typ    └────────┘└───────────────────────────────────────┘
doc    └────────┘ └───────────────────────────────────────┘
txt    └────────┘ └───────────────────────────────────────┘
par    └────────┘ └───────────────────────────────────────┘
pid              └─────────────────────┘└────────────────┘
st   ─────────────────────────────────────────────────────┘└─
797    { simp [zero_lt_one] },
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ───┘└─────────────────┘└┘
798    { simp [has], apply mul_pos, apply h0 a (mem_insert_self a s),
id             └─┘         └─────┘        └┘    └─────────────┘  
src      └────┘     └────┘└─────┘  └────┘    └─────────────┘  
typ      └────┘└─┘  └────┘└─────┘  └────┘└┘  └─────────────┘
doc      └────┘     └────┘         └────┘                     
txt      └────┘     └────┘         └────┘                     
par      └────┘     └────┘         └────┘                     
pid                                                       
st   ─────────────┘└─────────────┘└────────────────────────────────┘└─
799      exact ih (λ x H, h0 x (mem_insert_of_mem H)) }
id             └┘         └┘    └───────────────┘
src      └────┘    └────┘    └───────────────┘ └─┘
typ      └────┘└┘  └────┘└┘  └───────────────┘ └─┘
doc      └────┘    └────┘                      └─┘
txt      └────┘    └────┘                      └─┘
par      └────┘    └────┘                      └─┘
pid               └────┘                      └┘
st   ────────────────────────────────────────────────┘└─
800  end
st   ──┘
801  
802  /- this is also true for a ordered commutative multiplicative monoid -/
803  lemma prod_le_prod {s : finset α} {f g : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x)
id                           └────┘                      └┘          
src                          └────┘                                    
typ                          └────┘                      └┘          
doc                          └────┘
804    (h1 : ∀(x ∈ s), f x ≤ g x) : s.prod f ≤ s.prod g :=
id                          └───┘   └───┘ 
src                                 └───┘     └───┘
typ                         └───┘   └───┘ 
doc                                  └───┘      └───┘
805  begin
st   └─────
806    induction s using finset.induction with a s has ih h,
id               
src    └────────┘ └───────────────────────────────────────┘
typ    └────────┘└───────────────────────────────────────┘
doc    └────────┘ └───────────────────────────────────────┘
txt    └────────┘ └───────────────────────────────────────┘
par    └────────┘ └───────────────────────────────────────┘
pid              └─────────────────────┘└────────────────┘
st   ─────────────────────────────────────────────────────┘└─
807    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
808    { simp [has], apply mul_le_mul,
id             └─┘         └────────┘
src      └────┘     └────┘└────────┘
typ      └────┘└─┘  └────┘└────────┘
doc      └────┘     └────┘
txt      └────┘     └────┘
par      └────┘     └────┘
pid                    
st   ─────────────┘└────────────────┘└─
809        exact h1 a (mem_insert_self a s),
id               └┘    └─────────────┘  
src        └────┘    └─────────────┘  
typ        └────┘└┘  └─────────────┘
doc        └────┘                     
txt        └────┘                     
par        └────┘                     
pid                                  
st   ─────────────────────────────────────┘└─
810        apply ih (λ x H, h0 _ _) (λ x H, h1 _ _); exact (mem_insert_of_mem H),
id               └┘         └┘              └┘              └───────────────┘ 
src        └────┘    └────┘  └────┘  └────┘  └───┘  └────┘ └───────────────┘ 
typ        └────┘└┘  └────┘└┘└────┘  └────┘└┘└───┘  └────┘ └───────────────┘
doc        └────┘    └────┘  └────┘  └────┘  └───┘  └────┘                   
txt        └────┘    └────┘  └────┘  └────┘  └───┘  └────┘                   
par        └────┘    └────┘  └────┘  └────┘  └───┘  └────┘                   
pid                 └────┘  └────┘  └────┘  └───┘                          
st   ──────────────────────────────────────────────────────────────────────────┘└─
811        apply prod_nonneg (λ x H, h0 x (mem_insert_of_mem H)),
id               └─────────┘         └┘    └───────────────┘
src        └────┘└─────────┘  └────┘    └───────────────┘ └┘
typ        └────┘└─────────┘  └────┘└┘  └───────────────┘ └┘
doc        └────┘             └────┘                      └┘
txt        └────┘             └────┘                      └┘
par        └────┘             └────┘                      └┘
pid                          └────┘                      └┘
st   ──────────────────────────────────────────────────────────┘└─
812        apply le_trans (h0 a (mem_insert_self a s)) (h1 a (mem_insert_self a s)) }
id               └──────┘  └┘                           └┘    └─────────────┘  
src        └────┘└──────┘                      └─┘     └─────────────┘  └─┘
typ        └────┘└──────┘ └┘                   └─┘ └┘  └─────────────┘└─┘
doc        └────┘                              └─┘                      └─┘
txt        └────┘                              └─┘                      └─┘
par        └────┘                              └─┘                      └─┘
pid                                           └─┘                      └┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
813  end
st   ──┘
814  
815  end linear_ordered_comm_ring
816  
817  @[simp] lemma card_pi [decidable_eq α] {δ : α → Type*}
id                          └──────────┘        
src                         └──────────┘
typ                         └──────────┘        
doc    └──┘
818    (s : finset α) (t : Π a, finset (δ a)) :
id          └────┘            └────┘   
src         └────┘              └────┘
typ         └────┘            └────┘   
doc         └────┘              └────┘
819    (s.pi t).card = s.prod (λ a, card (t a)) :=
id      └─┘  └──┘   └───┘      └──┘   
src      └─┘   └──┘    └───┘       └──┘
typ     └─┘  └──┘   └───┘      └──┘   
doc            └──┘     └───┘       └──┘
820  multiset.card_pi _ _
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
821  
822  theorem card_le_mul_card_image [decidable_eq β] {f : α → β} (s : finset α)
id                                   └──────────┘                  └────┘ 
src                                  └──────────┘                     └────┘
typ                                  └──────────┘                  └────┘ 
doc                                                                   └────┘
823    (n : ℕ) (hn : ∀ a ∈ s.image f, (s.filter (λ x, f x = a)).card ≤ n) :
id                       └────┘    └─────┘           └──┘   
src                        └────┘      └─────┘               └──┘  
typ                      └────┘    └─────┘           └──┘   
doc                         └────┘      └─────┘                └──┘
824    s.card ≤ n * (s.image f).card :=
id     └───┘     └────┘  └──┘
src     └───┘       └────┘   └──┘
typ    └───┘     └────┘  └──┘
doc     └───┘         └────┘   └──┘
825  calc s.card = (s.image f).sum (λ a, (s.filter (λ x, f x = a)).card) :
id        └───┘    └────┘  └─┘        └─────┘           └──┘
src        └───┘     └────┘   └─┘          └─────┘               └──┘
typ       └───┘    └────┘  └─┘        └─────┘           └──┘
doc        └───┘     └────┘                └─────┘                └──┘
826    card_eq_sum_card_image _ _
id     └────────────────────┘
src    └────────────────────┘
typ    └────────────────────┘
827  ... ≤ (s.image f).sum (λ _, n) : sum_le_sum hn
id          └────┘  └─┘           └────────┘ └┘
src          └────┘   └─┘             └────────┘
typ         └────┘  └─┘           └────────┘ └┘
doc          └────┘
828  ... = _ : by simp [mul_comm]
id                      └──────┘
src               └────┘└──────┘└─
typ               └────┘└──────┘└─
doc               └────┘        └─
txt               └────┘        └─
par               └────┘        └─
pid                           
st               └────────────────
829  
src  
typ  
doc  
txt  
par  
pid  
st   
830  @[simp] lemma prod_Ico_id_eq_fact : ∀ n : ℕ, (Ico 1 n.succ).prod (λ x, x) = nat.fact n
id                                               └─┘   └───┘ └──┘          └──────┘ 
src                                               └─┘    └───┘ └──┘            └──────┘
typ                                              └─┘   └───┘ └──┘          └──────┘ 
doc    └──┘                                        └─┘          └──┘             └──────┘
831  | 0 := rfl
id          └─┘
src         └─┘
typ         └─┘
832  | (n+1) := by rw [prod_Ico_succ_top $ nat.succ_le_succ $ zero_le n,
id                    └───────────────┘   └──────────────┘   └─────┘ 
src               └──┘└───────────────┘ └──────────────┘ └─────┘ └─
typ               └──┘└───────────────┘ └──────────────┘ └─────┘└─
doc                └──┘                                           └─
txt                └──┘                                           └─
par                └──┘                                           └─
pid                  └┘                                           └─
st                └───────────────────────────────────────────────────┘└─
833    nat.fact_succ, prod_Ico_id_eq_fact n, nat.succ_eq_add_one, mul_comm]
id     └───────────┘  └─────────────────┘   └─────────────────┘  └──────┘
src  ─┘└───────────┘└┘                    └┘└─────────────────┘└┘└──────┘└─
typ  ─┘└───────────┘└┘└─────────────────┘└┘└─────────────────┘└┘└──────┘└─
doc  ─┘             └┘                    └┘                   └┘        └─
txt  ─┘             └┘                    └┘                   └┘        └─
par  ─┘             └┘                    └┘                   └┘        └─
pid  ─┘             └┘                    └┘                   └┘        
st   ──────────────┘└─────────────────────┘└───────────────────┘└────────┘
834  
src  
typ  
doc  
txt  
par  
pid  
st   
835  end finset
836  
837  
838  namespace finset
839  section gauss_sum
840  
841  /-- Gauss' summation formula -/
842  lemma sum_range_id_mul_two :
843    ∀(n : ℕ), (finset.range n).sum (λi, i) * 2 = n * (n - 1)
id              └──────────┘  └─┘                
src              └──────────┘   └─┘                    
typ             └──────────┘  └─┘                
doc               └──────────┘
844  | 0       := rfl
id                └─┘
src               └─┘
typ               └─┘
845  | 1       := rfl
id                └─┘
src               └─┘
typ               └─┘
846  | ((n + 1) + 1) :=
id             
src            
typ            
847    begin
st     └─────
848      rw [sum_range_succ, add_mul, sum_range_id_mul_two (n + 1), mul_comm, two_mul,
id           └────────────┘  └─────┘  └──────────────────┘        └──────┘  └─────┘
src      └──┘└────────────┘└┘└─────┘└┘                      └───┘└──────┘└┘└─────┘└─
typ      └──┘└────────────┘└┘└─────┘└┘└──────────────────┘ └───┘└──────┘└┘└─────┘└─
doc      └──┘              └┘       └┘                       └───┘        └┘       └─
txt      └──┘              └┘       └┘                       └───┘        └┘       └─
par      └──┘              └┘       └┘                       └───┘        └┘       └─
pid        └┘              └┘       └┘                       └───┘        └┘       └─
st   ─────────────────────┘└───────┘└────────────────────────────┘└────────┘└───────┘└─
849        nat.add_sub_cancel, nat.add_sub_cancel, mul_comm _ n],
id         └────────────────┘  └────────────────┘  └──────┘   
src  ─────┘└────────────────┘└┘└────────────────┘└┘└──────┘└─┘ 
typ  ─────┘└────────────────┘└┘└────────────────┘└┘└──────┘└─┘
doc  ─────┘                  └┘                  └┘        └─┘ 
txt  ─────┘                  └┘                  └┘        └─┘ 
par  ─────┘                  └┘                  └┘        └─┘ 
pid  ─────┘                  └┘                  └┘        └─┘ 
st   ───────────────────────┘└──────────────────┘└────────────┘└──
850      simp only [add_mul, one_mul, add_comm, add_assoc, add_left_comm]
id                  └─────┘  └─────┘  └──────┘  └───────┘  └───────────┘
src      └─────────┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ      └─────────┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc      └─────────┘       └┘       └┘        └┘         └┘             └─
txt      └─────────┘       └┘       └┘        └┘         └┘             └─
par      └─────────┘       └┘       └┘        └┘         └┘             └─
pid          └──┘└┘       └┘       └┘        └┘         └┘             
st   ─────────────────────────────────────────────────────────────────────
851    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
852  
853  /-- Gauss' summation formula -/
854  lemma sum_range_id (n : ℕ) : (finset.range n).sum (λi, i) = (n * (n - 1)) / 2 :=
id                                └──────────┘  └─┘                   
src                               └──────────┘   └─┘                       
typ                               └──────────┘  └─┘                   
doc                                └──────────┘
855  by rw [← sum_range_id_mul_two n, nat.mul_div_cancel]; exact dec_trivial
id            └──────────────────┘   └────────────────┘         └─────────┘
src     └────┘└──────────────────┘ └┘└────────────────┘  └────┘└─────────┘
typ     └────┘└──────────────────┘└┘└────────────────┘  └────┘└─────────┘
doc     └────┘└──────────────────┘ └┘                    └────┘└─────────┘
txt     └────┘                     └┘                    └────┘           
par     └────┘                     └┘                    └────┘           
pid       └──┘                     └┘                                    
st     └───────────────────────────┘└──────────────────┘└───────────────────
856  
src  
typ  
doc  
txt  
par  
pid  
st   
857  end gauss_sum
858  
859  lemma card_eq_sum_ones (s : finset α) : s.card = s.sum (λ _, 1) :=
id                               └────┘     └───┘  └──┘    
src                              └────┘       └───┘   └──┘
typ                              └────┘     └───┘  └──┘    
doc                              └────┘       └───┘
860  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
861  
src  
typ  
doc  
txt  
par  
pid  
st   
862  end finset
863  
864  section group
865  
866  open list
867  variables [group α] [group β]
id              └───┘     └───┘
src             └───┘     └───┘
typ             └───┘     └───┘
868  
869  theorem is_group_anti_hom.map_prod (f : α → β) [is_group_anti_hom f] (l : list α) :
id                                                 └───────────────┘        └──┘ 
src                                                  └───────────────┘         └──┘
typ                                                └───────────────┘        └──┘ 
doc                                                  └───────────────┘
870    f (prod l) = prod (map f (reverse l)) :=
id       └──┘    └──┘  └─┘   └─────┘ 
src       └──┘     └──┘  └─┘    └─────┘
typ      └──┘    └──┘  └─┘   └─────┘ 
doc       └──┘      └──┘
871  by induction l with hd tl ih; [exact is_group_anti_hom.map_one f,
id                                      └───────────────────────┘ 
src     └────────┘ └────────────┘  └────┘└───────────────────────┘
typ     └────────┘└────────────┘  └────┘└───────────────────────┘
doc     └────────┘ └────────────┘   └────┘                         
txt     └────────┘ └────────────┘   └────┘                         
par     └────────┘ └────────────┘   └────┘                         
pid               └───────────┘                                 
st     └───────────────────────────────────────────────────────────────
872    simp only [prod_cons, is_group_anti_hom.map_mul f, ih, reverse_cons, map_append, prod_append, map_singleton, prod_cons, prod_nil, mul_one]]
id                └───────┘  └───────────────────────┘   └┘  └──────────┘  └────────┘  └─────────┘  └───────────┘  └───────┘  └──────┘  └─────┘
src    └─────────┘└───────┘└┘└───────────────────────┘ └┘  └┘└──────────┘└┘└────────┘└┘└─────────┘└┘└───────────┘└┘└───────┘└┘└──────┘└┘└─────┘
typ    └─────────┘└───────┘└┘└───────────────────────┘└┘└┘└┘└──────────┘└┘└────────┘└┘└─────────┘└┘└───────────┘└┘└───────┘└┘└──────┘└┘└─────┘
doc    └─────────┘         └┘                          └┘  └┘            └┘          └┘           └┘             └┘         └┘        └┘       
txt    └─────────┘         └┘                          └┘  └┘            └┘          └┘           └┘             └┘         └┘        └┘       
par    └─────────┘         └┘                          └┘  └┘            └┘          └┘           └┘             └┘         └┘        └┘       
pid        └──┘└┘         └┘                          └┘  └┘            └┘          └┘           └┘             └┘         └┘        └┘       
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
873  
874  theorem inv_prod : ∀ l : list α, (prod l)⁻¹ = prod (map (λ x, x⁻¹) (reverse l)) :=
id                            └──┘    └──┘  └┘  └──┘  └─┘      └┘   └─────┘ 
src                           └──┘     └──┘   └┘  └──┘  └─┘        └┘   └─────┘
typ                           └──┘    └──┘  └┘  └──┘  └─┘      └┘   └─────┘ 
doc                                    └──┘        └──┘
875  λ l, @is_group_anti_hom.map_prod _ _ _ _ _ inv_is_group_anti_hom l -- TODO there is probably a cleaner proof of this
id        └────────────────────────┘           └───────────────────┘ 
src        └────────────────────────┘           └───────────────────┘
typ       └────────────────────────┘           └───────────────────┘ 
876  
877  end group
878  
879  @[to_additive]
doc    └─────────┘
880  lemma monoid_hom.map_prod [comm_monoid β] [comm_monoid γ] (g : β →* γ) (f : α → β) (s : finset α) :
id                              └─────────┘    └─────────┘         └┘                  └────┘ 
src                             └─────────┘     └─────────┘           └┘                     └────┘
typ                             └─────────┘    └─────────┘         └┘                  └────┘ 
doc                                                                   └┘                     └────┘
881    g (s.prod f) = s.prod (λx, g (f x)) :=
id       └───┘    └───┘        
src        └───┘      └───┘
typ      └───┘    └───┘        
doc        └───┘       └───┘
882  (s.prod_hom g).symm
id    └───────┘  └──┘
src    └───────┘   └──┘
typ   └───────┘  └──┘
883  
884  
885  @[to_additive is_add_group_hom_finset_sum]
doc    └─────────┘
886  lemma is_group_hom_finset_prod {α β γ} [group α] [comm_group β] (s : finset γ)
id                                           └───┘    └────────┘        └────┘ 
src                                          └───┘     └────────┘         └────┘
typ                                          └───┘    └────────┘        └────┘ 
doc                                                                       └────┘
887    (f : γ → α → β) [∀c, is_group_hom (f c)] : is_group_hom (λa, s.prod (λc, f c a)) :=
id                      └──────────┘        └──────────┘     └───┘       
src                         └──────────┘          └──────────┘       └───┘
typ                     └──────────┘        └──────────┘     └───┘       
doc                         └──────────┘          └──────────┘       └───┘
888  { map_mul := assume a b, by simp only [λc, is_mul_hom.map_mul (f c), finset.prod_mul_distrib] }
id                                            └────────────────┘       └─────────────────────┘
src                              └─────────┘ └─┘└────────────────┘   └─┘└─────────────────────┘└┘
typ                            └─────────┘ └─┘└────────────────┘  └─┘└─────────────────────┘└┘
doc                              └─────────┘ └─┘                     └─┘                       └┘
txt                              └─────────┘ └─┘                     └─┘                       └┘
par                              └─────────┘ └─┘                     └─┘                       └┘
pid                                  └──┘└┘ └─┘                     └─┘                       
st                              └─────────────────────────────────────────────────────────────────┘
889  
890  attribute [instance] is_group_hom_finset_prod is_add_group_hom_finset_sum
id                        └──────────────────────┘ └─────────────────────────┘
src                       └──────────────────────┘ └─────────────────────────┘
typ                       └──────────────────────┘ └─────────────────────────┘
891  
892  namespace multiset
893  variables [decidable_eq α]
id              └──────────┘
src             └──────────┘
typ             └──────────┘
894  
895  @[simp] lemma to_finset_sum_count_eq (s : multiset α) :
id                                             └──────┘ 
src                                            └──────┘
typ                                            └──────┘ 
doc    └──┘                                    └──────┘
896    s.to_finset.sum (λa, s.count a) = s.card :=
id     └────────┘└──┘     └────┘    └───┘
src     └────────┘└──┘       └────┘      └───┘
typ    └────────┘└──┘     └────┘    └───┘
doc     └────────┘           └────┘       └───┘
897  multiset.induction_on s rfl
id   └───────────────────┘  └─┘
src  └───────────────────┘   └─┘
typ  └───────────────────┘  └─┘
898    (assume a s ih,
id               └┘
typ              └┘
899      calc (to_finset (a :: s)).sum (λx, count x (a :: s)) =
id             └───────┘   └┘   └─┘      └───┘    └┘ 
src            └───────┘    └┘    └─┘       └───┘      └┘
typ            └───────┘   └┘   └─┘      └───┘    └┘ 
doc            └───────┘    └┘              └───┘      └┘
900        (to_finset (a :: s)).sum (λx, (if x = a then 1 else 0) + count x s) :
id          └───────┘   └┘   └─┘                             └───┘  
src         └───────┘    └┘    └─┘                                └───┘
typ         └───────┘   └┘   └─┘                             └───┘  
doc         └───────┘    └┘                                         └───┘
901          finset.sum_congr rfl $ λ _ _, by split_ifs;
id           └──────────────┘ └─┘      
src          └──────────────┘ └─┘             └───────┘
typ          └──────────────┘ └─┘           └───────┘
doc                                           └───────┘
txt                                           └───────┘
par                                           └───────┘
st                                           └───────────
902          [simp only [h, count_cons_self, nat.one_add], simp only [count_cons_of_ne h, zero_add]]
id                        └─────────────┘  └─────────┘              └──────────────┘   └──────┘
src          └─────────┘ └┘└─────────────┘└┘└─────────┘  └─────────┘└──────────────┘ └┘└──────┘
typ          └─────────┘└┘└─────────────┘└┘└─────────┘  └─────────┘└──────────────┘└┘└──────┘
doc           └─────────┘ └┘               └┘             └─────────┘                 └┘        
txt           └─────────┘ └┘               └┘             └─────────┘                 └┘        
par           └─────────┘ └┘               └┘             └─────────┘                 └┘        
pid               └──┘└┘ └┘               └┘                 └──┘└┘                 └┘        
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘
903        ... = card (a :: s) :
id               └──┘   └┘ 
src              └──┘    └┘
typ              └──┘   └┘ 
doc              └──┘    └┘
904        begin
st         └─────
905          by_cases a ∈ s.to_finset,
id                      └─────────┘
src          └───────┘ └─────────┘
typ          └───────┘└─────────┘
doc          └───────┘  └─────────┘
txt          └───────┘  
par          └───────┘  
pid                    
st   ───────────────────────────────┘└─
906          { have : (to_finset s).sum (λx, ite (x = a) 1 0) = (finset.singleton a).sum (λx, ite (x = a) 1 0),
id                     └───────┘                               └──────────────┘             └─┘      
src            └─────┘ └───────┘ └────┘  └─┘      └─────┘  └──────────────┘ └────┘  └─┘└─┘    └────┘
typ            └─────┘ └───────┘└────┘  └─┘      └─────┘  └──────────────┘ └────┘  └─┘└─┘   └────┘
doc            └─────┘ └───────┘ └────┘  └─┘       └─────┘  └──────────────┘ └────┘  └─┘       └────┘
txt            └─────┘           └────┘  └─┘       └─────┘                   └────┘  └─┘       └────┘
par            └─────┘           └────┘  └─┘       └─────┘                   └────┘  └─┘       └────┘
pid            └───┘└┘           └────┘  └─┘       └─────┘                   └────┘  └─┘       └────┘
st   ─────────┘└─────────────────────────────────────────────────────────────────────────────────────────────┘└─
907            { apply (finset.sum_subset _ _).symm,
id                      └───────────────┘
src              └────┘ └───────────────┘└────────┘
typ              └────┘ └───────────────┘└────────┘
doc              └────┘                  └────────┘
txt              └────┘                  └────────┘
par              └────┘                  └────────┘
pid                                     └───────┘
st   ───────────┘└────────────────────────────────┘└─
908              { intros _ H, rwa mem_singleton.1 H },
id                                 └───────────┘   
src                └────────┘  └──┘└───────────┘└─┘ 
typ                └────────┘  └──┘└───────────┘└─┘
doc                └────────┘  └──┘             └─┘ 
txt                └────────┘  └──┘             └─┘ 
par                └────────┘  └──┘             └─┘ 
pid                      └──┘                  └─┘ 
st   ─────────────┘└────────┘└──────────────────────┘└┘
909              { exact λ _ _ H, if_neg (mt finset.mem_singleton.2 H) } },
id                                └────┘  └┘ └──────────────────┘
src                └────┘ └──────┘└────┘ └┘└──────────────────┘└─┘ └┘
typ                └────┘ └──────┘└────┘ └┘└──────────────────┘└─┘ └┘
doc                └────┘ └──────┘                             └─┘ └┘
txt                └────┘ └──────┘                             └─┘ └┘
par                └────┘ └──────┘                             └─┘ └┘
pid                      └──────┘                             └─┘ 
st   ─────────────────────────────────────────────────────────────────┘└──┘
910            rw [to_finset_cons, finset.insert_eq_of_mem h, finset.sum_add_distrib, ih, this, finset.sum_singleton, if_pos rfl, add_comm, card_cons] },
id                 └────────────┘  └─────────────────────┘   └────────────────────┘  └┘  └──┘  └──────────────────┘  └────┘ └─┘  └──────┘  └───────┘
src            └──┘└────────────┘└┘└─────────────────────┘ └┘└────────────────────┘└┘  └┘    └┘└──────────────────┘└┘└────┘└─┘└┘└──────┘└┘└───────┘└┘
typ            └──┘└────────────┘└┘└─────────────────────┘└┘└────────────────────┘└┘└┘└┘└──┘└┘└──────────────────┘└┘└────┘└─┘└┘└──────┘└┘└───────┘└┘
doc            └──┘              └┘                        └┘                      └┘  └┘    └┘                    └┘         └┘        └┘         └┘
txt            └──┘              └┘                        └┘                      └┘  └┘    └┘                    └┘         └┘        └┘         └┘
par            └──┘              └┘                        └┘                      └┘  └┘    └┘                    └┘         └┘        └┘         └┘
pid              └┘              └┘                        └┘                      └┘  └┘    └┘                    └┘         └┘        └┘         
st   ───────────────────────────┘└─────────────────────────┘└──────────────────────┘└──┘└────┘└────────────────────┘└──────────┘└────────┘└─────────┘└┘
911          { have ha : a ∉ s, by rwa mem_to_finset at h,
id                                   └───────────┘
src            └────────┘        └──┘└───────────┘└───┘
typ            └────────┘      └──┘└───────────┘└───┘
doc            └────────┘        └──┘             └───┘
txt            └────────┘        └──┘             └───┘
par            └────────┘        └──┘             └───┘
pid            └─────┘└─┘                        └───┘
st   ────────────────────────┘         └───────────┘     └─
912            have : (to_finset s).sum (λx, ite (x = a) 1 0) = (to_finset s).sum (λx, 0), from
id                                           └─┘                └───────┘ 
src            └─────┘           └────┘  └─┘└─┘    └─────┘  └───────┘ └────┘  └───┘  └────
typ            └─────┘           └────┘  └─┘└─┘   └─────┘  └───────┘└────┘  └───┘  └────
doc            └─────┘           └────┘  └─┘       └─────┘  └───────┘ └────┘  └───┘  └────
txt            └─────┘           └────┘  └─┘       └─────┘            └────┘  └───┘  └────
par            └─────┘           └────┘  └─┘       └─────┘            └────┘  └───┘  └────
pid            └───┘└┘           └────┘  └─┘       └─────┘            └────┘  └───┘  └────
st   ───────────────────────────────────────────────────────────────────────────────────┘└──────
913              finset.sum_congr rfl (λ x hx, if_neg $ by rintro rfl; cc),
id               └──────────────┘ └─┘          └────┘
src  ───────────┘└──────────────┘└─┘  └─────┘└────┘   └────────┘└┘└┘
typ  ───────────┘└──────────────┘└─┘  └─────┘└────┘   └────────┘└┘└┘
doc  ───────────┘                     └─────┘         └────────┘└┘└┘
txt  ───────────┘                     └─────┘         └────────┘└┘└┘
par  ───────────┘                     └─────┘         └────────┘└┘└┘
pid  ───────────┘                     └─────┘         └──────────────┘
st   ────────────────────────────────────────────────────┘└─────────────┘└─
914            rw [to_finset_cons, finset.sum_insert h, if_pos rfl, finset.sum_add_distrib, this, finset.sum_const_zero, ih, count_eq_zero_of_not_mem ha, zero_add, add_comm, card_cons] }
id                 └────────────┘  └───────────────┘   └────┘ └─┘  └────────────────────┘  └──┘  └───────────────────┘  └┘  └──────────────────────┘ └┘  └──────┘  └──────┘  └───────┘
src            └──┘└────────────┘└┘└───────────────┘ └┘└────┘└─┘└┘└────────────────────┘└┘    └┘└───────────────────┘└┘  └┘└──────────────────────┘  └┘└──────┘└┘└──────┘└┘└───────┘└┘
typ            └──┘└────────────┘└┘└───────────────┘└┘└────┘└─┘└┘└────────────────────┘└┘└──┘└┘└───────────────────┘└┘└┘└┘└──────────────────────┘└┘└┘└──────┘└┘└──────┘└┘└───────┘└┘
doc            └──┘              └┘                  └┘         └┘                      └┘    └┘                     └┘  └┘                          └┘        └┘        └┘         └┘
txt            └──┘              └┘                  └┘         └┘                      └┘    └┘                     └┘  └┘                          └┘        └┘        └┘         └┘
par            └──┘              └┘                  └┘         └┘                      └┘    └┘                     └┘  └┘                          └┘        └┘        └┘         └┘
pid              └┘              └┘                  └┘         └┘                      └┘    └┘                     └┘  └┘                          └┘        └┘        └┘         
st   ───────────────────────────┘└───────────────────┘└──────────┘└──────────────────────┘└────┘└─────────────────────┘└──┘└───────────────────────────┘└────────┘└────────┘└─────────┘└─
915        end)
st   ────────┘
916  
917  end multiset
918  
919  namespace with_top
920  open finset
921  variables [decidable_eq α]
id              └──────────┘
src             └──────────┘
typ             └──────────┘
922  
923  /-- sum of finte numbers is still finite -/
924  lemma sum_lt_top [ordered_comm_monoid β] {s : finset α} {f : α → with_top β} :
id                     └─────────────────┘        └────┘           └──────┘ 
src                    └─────────────────┘         └────┘             └──────┘
typ                    └─────────────────┘        └────┘           └──────┘ 
doc                    └─────────────────┘         └────┘
925    (∀a∈s, f a < ⊤) → s.sum f < ⊤ :=
id                 └──┘   
src                     └──┘    
typ                └──┘   
926  finset.induction_on s (by { intro h, rw sum_empty, exact coe_lt_top _ })
id   └─────────────────┘                    └───────┘        └────────┘
src  └─────────────────┘         └─────┘  └─┘└───────┘  └────┘└────────┘└─┘
typ  └─────────────────┘        └─────┘  └─┘└───────┘  └────┘└────────┘└─┘
doc  └─────────────────┘         └─────┘  └─┘           └────┘          └─┘
txt                              └─────┘  └─┘           └────┘          └─┘
par                              └─────┘  └─┘           └────┘          └─┘
pid                                   └┘                              └┘
st                            └────────┘└────────────┘└───────────────────┘└┘
927    (λa s ha ih h,
id         └┘ └┘ 
typ        └┘ └┘ 
928    begin
st     └─────
929      rw [sum_insert ha, add_lt_top], split,
id           └────────┘ └┘  └────────┘
src      └──┘└────────┘  └┘└────────┘  └───┘
typ      └──┘└────────┘└┘└┘└────────┘  └───┘
doc      └──┘            └┘            └───┘
txt      └──┘            └┘            └───┘
par      └──┘            └┘            └───┘
pid        └┘            └┘          
st   ────────────────────┘└──────────┘└──────┘└─
930      { apply h, apply mem_insert_self },
id                        └─────────────┘
src        └────┘   └────┘└─────────────┘
typ        └────┘   └────┘└─────────────┘
doc        └────┘   └────┘               
txt        └────┘   └────┘               
par        └────┘   └────┘               
pid                                    
st   ─────┘└─────┘└──────────────────────┘└┘
931      { apply ih, intros a ha, apply h, apply mem_insert_of_mem ha }
id                                               └───────────────┘ └┘
src        └────┘    └─────────┘  └────┘   └────┘└───────────────┘  
typ        └────┘    └─────────┘  └────┘   └────┘└───────────────┘└┘
doc        └────┘    └─────────┘  └────┘   └────┘                   
txt        └────┘    └─────────┘  └────┘   └────┘                   
par        └────┘    └─────────┘  └────┘   └────┘                   
pid                       └───┘                                  
st   ─────────────┘└───────────┘└───────┘└───────────────────────────┘└─
932    end)
st   ────┘
933  
934  /-- sum of finte numbers is still finite -/
935  lemma sum_lt_top_iff [canonically_ordered_monoid β] {s : finset α} {f : α → with_top β} :
id                         └────────────────────────┘        └────┘           └──────┘ 
src                        └────────────────────────┘         └────┘             └──────┘
typ                        └────────────────────────┘        └────┘           └──────┘ 
doc                        └────────────────────────┘         └────┘
936    s.sum f < ⊤ ↔ (∀a∈s, f a < ⊤) :=
id     └──┘             
src     └──┘                  
typ    └──┘             
937  iff.intro (λh a ha, lt_of_le_of_lt (single_le_sum (λa ha, zero_le _) ha) h) sum_lt_top
id   └───────┘     └┘  └────────────┘  └───────────┘    └┘  └─────┘    └┘    └────────┘
src  └───────┘           └────────────┘  └───────────┘         └─────┘           └────────┘
typ  └───────┘     └┘  └────────────┘  └───────────┘    └┘  └─────┘    └┘    └────────┘
doc                                                                              └────────┘
938  
939  end with_top